perm filename PROVE2.NEW[1,JRA]1 blob
sn#005875 filedate 1972-10-19 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP NEWPROOF
00400 (NIL NEWPROOF
00500 ALLPOS
00600 RESTRAT
00700 RESTRAT1
00800 RESTRAT2
00900 RESTRATS
01000 ALLNEG
01100 ANCESTOR
01200 APPLYTEMP
01300 APPTEMP
01400 BARF
01500 SEARCH1
01600 CONST
01700 HERE
01800 VAR
01900 ISCLS
02000 ISCL
02100 ISLIT
02200 ISTRM
02300 MKWRD
02400 NEG
02500 NEGBIT
02600 POS
02700 POSBIT
02800 SEARCH
02900 NUM
03000 NEGL
03100 ANCESTRY
03200 APPENDIT
03300 ANDOR
03400 ASSOC1
03500 ATTEMPT
03600 ATTEMPTUNTIL
03700 ATTEMPT1
03800 AUTO
03900 BAKSUB
04000 BOOKEEP
04100 CHOICE
04200 CHOICE1
04300 CLAUSES
04400 CLAUSES2
04500 CLAUSES1
04600 CNF
04700 CNF1
04800 CNF2
04900 CNF3
05000 CNVT
05100 CNVT2
05200 CNVT3
05300 COPY
05400 COPYDELETED
05500 DEMOD
05600 DEM
05700 DEPTH
05800 DEPTH1
05900 DEL
06000 DOML
06100 DOMC
06200 DOWN
06300 EDIT
06400 ERPRINT
06500 ERPRIN1
06600 EXPUNGE
06700 FINI
06800 FIRSTS
06900 FIXNEG
07000 FIXQFF
07100 FIXQFF1
07200 GENSKOLEM
07300 GETNAME
07400 GETVARS
07500 GOLIST
07600 GOLIST1
07700 INCLAUSES
07800 INITIAL
07900 INITIALAX
08000 INITIALAX1
08100 MAPIT
08200 MATCHER
08300 MATCH1
08400 MATCHTR
08500 MATCHPN
08600 MATMLT
08700 MATMLT*
08800 MAX
08900 MEMC
09000 MIN1
09100 MINIMIZE
09200 MIN
09300 MKSYM
09400 MODEL
09500 NCONC1
09600 NEGATE
09700 NEGSGN
09800 NOSYM
09900 OCR
10000 OCR1
10100 ONEGSGN
10200 *NOPOINT
10300 OCCUR
10400 ORDER
10500 ORDEREQUAL
10600 PARMOD
10700 PARMOD1
10800 POTZ
10900 PRECNF
11000 PROOF1
11100 PROVE
11200 PRPAR
11300 PRFPRINT
11400 PRFPR1
11500 PROOF
11600 PTRS
11700 QUERY
11800 REAL-LNGTH
11900 REDUCER
12000 REENTER
12100 RESTORE
12200 RESTORE1
12300 RESOLVE
12400 RESTS
12500 RESOLVE1
12600 RESTART
12700 RESET
12800 RESET1
12900 SAVE
13000 SAVE1
13100 SET1
13200 SET2
13300 SET3
13400 SETUP
13500 SEARCH2
13600 S2
13700 SETQUERY
13800 SETQUERY1
13900 SETQUERY2
14000 SUBS3TA
14100 SUBS3T**
14200 SUB*
14300 SUBSKOL
14400 SUPPORT
14500 SUBSUME1
14600 SUBS2T
14700 SUBS3T
14800 SUBSUME
14900 SUBSUME*
15000 SUBST1
15100 TCOPY
15200 TEMPLATE
15300 TERMS
15400 TERMS1
15500 TERMS2
15600 TIMEIT
15700 TREE
15800 TREEDEP
15900 TRY
16000 TRY1
16100 TRYPRF
16200 TRAVERSE
16300 UNIT
16400 UNITS
16500 UNITRES
16600 UNITREDUCT
16700 UNITPN
16800 UNIFY
16900 UNI
17000 UNION
17100 UNWIND
17200 UPDATE
17300 UPGETL
17400 UPGETNU
17500 UPDATESTATE
17600 UPIT
17700 UPIT1
17800 UP1A
17900 UP1B
18000 VARIT
18100 VINE
18200 <)
18300 VALUE)
18400
18500 (DEFPROP ALLPOS
18600 (LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
18700 MACRO)
18800
18900 (DEFPROP RESTRAT
19000 (LAMBDA(L)
19100 (LIST (QUOTE COND)
19200 (LIST (LIST (QUOTE NULL) (CADR L))
19300 (LIST (QUOTE RESTRAT1) (CADR L) (CADDR L))
19400 (LIST (QUOTE GO) (CADDDR L)))))
19500 MACRO)
19600
19700 (DEFPROP RESTRAT1
19800 (LAMBDA(L)
19900 (LIST (QUOTE COND)
20000 (LIST (LIST (QUOTE EQ) (LIST (QUOTE SETQ) (CADR L) (QUOTE (READ))) (QUOTE ESCAPE))
20100 (QUOTE (PRINT (QUOTE RESETTING-TO:)))
20200 (LIST (QUOTE GO) (CADDR L)))))
20300 MACRO)
20400
20500 (DEFPROP RESTRAT2
20600 (LAMBDA(M)
20700 (LIST (QUOTE COND)
20800 (LIST (QUOTE (EQ (SETQ Z6 (READ)) (QUOTE Y))) (LIST (QUOTE RESTRAT1) (CADR M) (CADDR M)))
20900 (LIST (QUOTE (EQ Z6 ESCAPE)) (QUOTE (PRINT (QUOTE RESETTING-TO))) (LIST (QUOTE GO) (CADDR M)))))
21000 MACRO)
21100
21200 (DEFPROP RESTRATS
21300 (LAMBDA(L)
21400 (LIST (QUOTE COND)
21500 (LIST (LIST (QUOTE EQ) (LIST (QUOTE SETQ) (CADR L) (QUOTE (READ))) (QUOTE ESCAPE))
21600 (QUOTE (PRINT (QUOTE RESETTING-TO:)))
21700 (LIST (QUOTE GO) (CADDR L)))))
21800 MACRO)
21900
22000 (DEFPROP ALLNEG
22100 (LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
22200 MACRO)
22300
22400 (DEFPROP ANCESTOR
22500 (LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
22600 MACRO)
22700
22800 (DEFPROP APPLYTEMP
22900 (LAMBDA(L)
23000 (PROG (Z L1 S)
23100 (SETQ S (CDR (ASSOC (CAR L) TEMPLATELIST)))
23200 (COND
23300 ((NOT (EQ (LENGTH (CAR S)) (LENGTH (CDR L))))
23400 (PRINT (QUOTE MISMATCH-IN-TEMPLATE-VARIABLES))
23500 (ERR NIL)))
23600 (SETQ L1 (CDR L))
23700 A (SETQ Z (NCONC (APPTEMP (FIRSTS L1) S) Z))
23800 (SETQ L1 (RESTS L1))
23900 (COND ((NULL L1) (RETURN Z)))
24000 (GO A)))
24100 FEXPR)
24200
24300 (DEFPROP APPTEMP
24400 (LAMBDA(L TEMP)
24500 (PROG (L2 L3)
24600 (SETQ L3 (CAR TEMP))
24700 (SETQ L2 (CDR TEMP))
24800 A (SETQ L2 (SUBST (CAR L) (CAR L3) L2))
24900 (SETQ L (CDR L))
25000 (SETQ L3 (CDR L3))
25100 (COND (L3 (GO A)))
25200 (RETURN L2)))
25300 EXPR)
25400
25500 (DEFPROP BARF
25600 (LAMBDA (L) (QUOTE (PRINT (QUOTE (DO YOU WANT TO CHANGE IT (Y / N))))))
25700 MACRO)
25800
25900 (DEFPROP SEARCH1
26000 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
26100 MACRO)
26200
26300 (DEFPROP CONST
26400 (LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
26500 MACRO)
26600
26700 (DEFPROP HERE
26800 (LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
26900 MACRO)
27000
27100 (DEFPROP VAR
27200 (LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
27300 MACRO)
27400
27500 (DEFPROP ISCLS
27600 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
27700 MACRO)
27800
27900 (DEFPROP ISCL
28000 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
28100 MACRO)
28200
28300 (DEFPROP ISLIT
28400 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
28500 MACRO)
28600
28700 (DEFPROP ISTRM
28800 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
28900 MACRO)
29000
29100 (DEFPROP MKWRD
29200 (LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
29300 MACRO)
29400
29500 (DEFPROP NEG
29600 (LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
29700 MACRO)
29800
29900 (DEFPROP NEGBIT
30000 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
30100 MACRO)
30200
30300 (DEFPROP POS
30400 (LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
30500 MACRO)
30600
30700 (DEFPROP POSBIT
30800 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
30900 MACRO)
31000
31100 (DEFPROP SEARCH
31200 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
31300 MACRO)
31400
31500 (DEFPROP NUM
31600 (LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
31700 MACRO)
31800
31900 (DEFPROP NEGL
32000 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
32100 MACRO)
32200
32300 (DEFPROP ANCESTRY
32400 (LAMBDA(LLST)
32500 (PROG (Z1 Z2 R M)
32600 (SETQ CNT (ADD1 (LENGTH CLAUSES)))
32700 TRY3 (COND ((NOT (HERE (CAR EE))) (GO TRY7)))
32800 (SETQ M (CHOICE1 (CAR EE) LLST))
32900 (COND ((NULL M) (GO TRY7)))
33000 (SETQ Z1 (CAR EE))
33100 TRY2 (SETQ Z2 (CAR M))
33200 (COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
33300 TRY1 (COND ((NOT STRATEGY) (GO TRY1A)))
33400 (COND ((STRATEGY Z1 Z2) (GO TRY1A)) (T (GO TRY6FA)))
33500 TRY1A
33600 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
33700 (SETQ R (RESOLVE Z1 Z2))
33800 (COND ((NULL R) (GO TRY6A)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
33900 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
34000 TRY6A
34100 TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6FA)))
34200 (SETQ R (PARMOD Z1 Z2))
34300 (COND ((NULL R) (GO TRY6FA)))
34400 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
34500 TRY6FA
34600 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
34700 (SETQ M (CDR M))
34800 (COND (M (GO TRY2)))
34900 TRY7 (SETQ EE (CDR EE))
35000 (COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
35100 TRY12
35200 (PRINT (QUOTE COUNT))
35300 (PRINT COUNT)
35400 (PRINT (QUOTE LEVEL))
35500 (PRINT LVL)
35600 (SETQ LVL (ADD1 LVL))
35700 (PRINT (QUOTE ELAPSED-TIME))
35800 (PRINT (TIMEIT))
35900 (COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
36000 (PRINT (QUOTE NO-PROOF-FOUND))
36100 (COND (AUTO (ERR (QUOTE NOPROOF))))
36200 (UPDATE CLAUSES)
36300 (COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
36400 (ERR (QUOTE NOPROOF))))
36500 EXPR)
36600
36700 (DEFPROP ANCESTRY
36800 (NIL . T)
36900 VALUE)
37000
37100 (DEFPROP APPENDIT
37200 (LAMBDA(X Y)
37300 (PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
37400 EXPR)
37500
37600 (DEFPROP ANDOR
37700 (LAMBDA(C UNL EXL PF)
37800 (PROG (Z1 Z2)
37900 (SETQ Z1 (CADR C))
38000 (SETQ Z2 (CADDR C))
38100 (COND
38200 ((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
38300 (RETURN (LIST (QUOTE AND) Z1 Z2)))
38400 ((EQ (CAR Z1) (QUOTE AND))
38500 (RETURN
38600 (LIST (QUOTE AND)
38700 (CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
38800 (CNF1 (LIST (QUOTE OR) (CADDR Z1) Z2) UNL EXL T))))
38900 ((EQ (CAR Z2) (QUOTE AND))
39000 (RETURN
39100 (LIST (QUOTE AND)
39200 (CNF1 (LIST (QUOTE OR) (CADR Z2) Z1) UNL EXL T)
39300 (CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
39400 (T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
39500 EXPR)
39600
39700 (DEFPROP ASSOC1
39800 (LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
39900 EXPR)
40000
40100 (DEFPROP ATTEMPT
40200 (LAMBDA(Z S C)
40300 (PROG (NEWNAME SUPPORT
40400 EDITSTRAT
40500 LCL
40600 LVL
40700 CNT
40800 XYZ2
40900 LSTCLS
41000 LLST
41100 Z1
41200 MERGE
41300 ORDER
41400 DEBUG
41500 DEPTH
41600 LENGTH
41700 ANCESTRY
41800 STRATEGY
41900 STRAT
42000 PMODEL
42100 NMODEL
42200 PFLG
42300 EQUAL
42400 PDEPTH
42500 DLIST
42600 XYZ
42700 XYZ1
42800 COND
42900 UNAXP
43000 UNAXN
43100 SAT
43200 EE
43300 EE1
43400 XX
43500 CLAUSES
43600 SUBCLAUSES
43700 COUNT)
43800 (SETQ TBL (SET1 (APPEND PREFN INFN)))
43900 (SET3 Z)
44000 (SETQ Z (MINIMIZE Z))
44100 (SETQ NEWNAME (INITIAL Z))
44200 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
44300 (SETQ COND C)
44400 (SETQ XYZ2 Z)
44500 (SETQ LVL 1)
44600 (SETQ COUNT 0)
44700 (SETQ Z (UNITPN XYZ2))
44800 (SETQ UNAXP (CAR Z))
44900 (SETQ UNAXN (CDR Z))
45000 (SETQ CLAUSES XYZ2)
45100 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
45200 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
45300 (T (SETQ SUBCLAUSES CLAUSES)))
45400 (SETQ LCL (LAST CLAUSES))
45500 (SETQ LSTCLS LCL)
45600 (COND (ANCESTRY (GO AA)))
45700 (SETQ XX (CONS CLAUSES CLAUSES))
45800 (SETQ EE CLAUSES)
45900 (SETQ EE1 (LAST EE))
46000 (SETQ CNT (LENGTH XYZ2))
46100 BB (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
46200 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
46300 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
46400 (EVAL
46500 (LIST (QUOTE OUTC)
46600 (LIST (QUOTE OUTPUT)
46700 (QUOTE PRF)
46800 (QUOTE DSK:)
46900 (CONS (READLIST
47000 (CONS (QUOTE #)
47100 (CONS (SETQ PRNO (ADD1 PRNO))
47200 FILENAM)))
47300 (QUOTE PRF)))
47400 NIL)))
47500 (QUERY)
47600 (PROOF LHP RHP)
47700 (OUTC Z T)
47800 (RETURN Z1))
47900 (T (RETURN Z1)))
48000 AA (SETQ XYZ XYZ2)
48100 (SETQ EE CLAUSES)
48200 (SETQ EE1 (LAST CLAUSES))
48300 CC (SETQ LLST (CONS (CAR XYZ) LLST))
48400 (SETQ XYZ (CDR XYZ))
48500 (COND (XYZ (GO CC)) (T (GO BB)))))
48600 EXPR)
48700
48800 (DEFPROP ATTEMPTUNTIL
48900 (LAMBDA (L S C) (ATTEMPT (INITIALAX L) S C))
49000 EXPR)
49100
49200 (DEFPROP ATTEMPT1
49300 (LAMBDA (L) (COND (ANCESTRY (ANCESTRY LLST)) (T (TRYPRF L))))
49400 EXPR)
49500
49600 (DEFPROP AUTO
49700 (LAMBDA(XX)
49800 (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
49900 (COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
50000 (SETQ PDEPTH 3)
50100 (SETQ DDEPTH 4)
50200 (COND
50300 ((NULL EQUAL) (PRINT (QUOTE (IS THERE AN EQUALITY PREDICATE (Y / N))))
50400 (COND
50500 ((EQ (READ) (QUOTE Y)) (PRINT (QUOTE (WHAT IS IT)))
50600 (SETQ PFLG NIL)
50700 (SETQ EQUAL (READ))))))
50800 (SETQ X1 XX)
50900 (SETQ M (SETQ D 0))
51000 A (SETQ M (MAX M (LENGTH (CDAR X1))))
51100 (SETQ D (MAX D (DEPTH (CDAR X1))))
51200 (SETQ Z2 (CAR X1))
51300 (COND
51400 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
51500 (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
51600 (SETQ X1 (CDR X1))
51700 (COND ((CDR X1) (GO A)))
51800 (SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
51900 (COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
52000 B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
52100 C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
52200 ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
52300 (COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
52400 (COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
52500 (COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
52600 (COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))))
52700 (SETQ ANCESTRY T)
52800 (SETQ EDITSTRAT
52900 (QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
53000 (SETQ DEBUG T)
53100 (COND (DLIST (SET3 DLIST)))
53200 (RETURN
53300 (LIST STRATEGY
53400 SUPPORT
53500 EDITSTRAT
53600 MERGE
53700 ORDER
53800 DEBUG
53900 DEPTH
54000 LENGTH
54100 ANCESTRY
54200 PMODEL
54300 NMODEL
54400 PFLG
54500 EQUAL
54600 PDEPTH
54700 DLIST))))
54800 EXPR)
54900
55000 (DEFPROP AUTO
55100 (NIL . T)
55200 VALUE)
55300
55400 (DEFPROP BAKSUB
55500 (LAMBDA(L R)
55600 (PROG (Z U1 U4)
55700 (SETQ Z L)
55800 ED4 (COND ((NOT Z) (RETURN NIL)) ((NOT (HERE (CAR Z))) (GO ED6A)))
55900 (SETQ U1 R)
56000 ED3 (SETQ U4 (CAR Z))
56100 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
56200 ED6 (SETQ U1 (CDR U1))
56300 (COND (U1 (GO ED1)))
56400 ED6A (SETQ Z (CDR Z))
56500 (GO ED4)
56600 ED2 (DEL U4)
56700 (GO ED4)))
56800 EXPR)
56900
57000 (DEFPROP BOOKEEP
57100 (LAMBDA(L M N)
57200 (PROG (U)
57300 B1 (SETQ U M)
57400 B3 (RPLACD (CDAAR U) (CONS 0 N))
57500 (SETQ U (CDR U))
57600 (COND ((NULL U) (RETURN (NCONC L M))))
57700 (GO B3)))
57800 EXPR)
57900
58000 (DEFPROP CHOICE
58100 (LAMBDA(X E E1)
58200 (PROG (Z1 Z2)
58300 (SETQ Z1 (CAR X))
58400 (SETQ Z2 (CDR X))
58500 B (COND ((EQ Z2 E1) (GO A)) (T (RETURN (RPLACD X (CDR Z2)))))
58600 A (SETQ Z1 (CDR Z1))
58700 (COND ((EQ Z1 E1) (RETURN T)) (T (RETURN (PROG2 (RPLACA X Z1) (RPLACD X E)))))))
58800 EXPR)
58900
59000 (DEFPROP CHOICE1
59100 (LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
59200 EXPR)
59300
59400 (DEFPROP CLAUSES
59500 (LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
59600 EXPR)
59700
59800 (DEFPROP CLAUSES2
59900 (LAMBDA (U) (CLAUSES1 U CNT))
60000 EXPR)
60100
60200 (DEFPROP CLAUSES1
60300 (LAMBDA(U N)
60400 (PROG NIL
60500 (COND ((NOT DEBUG) (RETURN NIL)))
60600 (COND ((NULL (CAR U)) (RETURN NIL)))
60700 CL1 (COND ((NULL U) (RETURN NIL)))
60800 (UP1A (CAR U) N)
60900 CL2 (SETQ U (CDR U))
61000 (SETQ N (ADD1 N))
61100 (GO CL1)))
61200 EXPR)
61300
61400 (DEFPROP CNF
61500 (LAMBDA(C1)
61600 (PROG (C)
61700 (SETQ C (PRECNF C1))
61800 (RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
61900 EXPR)
62000
62100 (DEFPROP CNF1
62200 (LAMBDA(C UNL EXL PF)
62300 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
62400 ((MEMQ (CAR C) (QUOTE (AND OR)))
62500 (ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
62600 ((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
62700 (CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
62800 ((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
62900 (CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
63000 (PF (SUBSKOL C EXL))
63100 (T (CONS ESCAPE (SUBSKOL C EXL)))))
63200 EXPR)
63300
63400 (DEFPROP CNF2
63500 (LAMBDA(C)
63600 (COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
63700 ((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
63800 (T (LIST (LIST C)))))
63900 EXPR)
64000
64100 (DEFPROP CNF3
64200 (LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
64300 EXPR)
64400
64500 (DEFPROP CNVT
64600 (LAMBDA(Z)
64700 (PROG (ZP ZN VARL VARNO)
64800 (SETQ VARNO 0)
64900 (COND
65000 ((EQ (LENGTH Z) 1)
65100 (RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
65200 A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
65300 (SETQ ZP (CNVT2 (CAR Z)))
65400 AP1 (SETQ Z (CDR Z))
65500 (COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
65600 (SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
65700 (GO AP1)
65800 AN1 (SETQ ZN (CNVT2 (CDAR Z)))
65900 AN1B (SETQ Z (CDR Z))
66000 AN1A (COND ((NULL Z) (GO AN2)))
66100 (SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
66200 (GO AN1B)
66300 AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
66400 ((NULL ZN) (RETURN ZP))
66500 (T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
66600 EXPR)
66700
66800 (DEFPROP CNVT2
66900 (LAMBDA(X)
67000 (COND ((ATOM X) X)
67100 ((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
67200 ((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
67300 (T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
67400 EXPR)
67500
67600 (DEFPROP CNVT3
67700 (LAMBDA(X)
67800 (PROG (Z)
67900 (SETQ Z (ASSOC X VARL))
68000 (COND (Z (RETURN (CDR Z))))
68100 (SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
68200 (RETURN VARNO)))
68300 EXPR)
68400
68500 (DEFPROP COPY
68600 (LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
68700 EXPR)
68800
68900 (DEFPROP COPYDELETED
69000 (LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
69100 EXPR)
69200
69300 (DEFPROP DEMOD
69400 (LAMBDA(X L)
69500 (PROG (S1 S2)
69600 B (SETQ S1 (CDAR X))
69700 A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
69800 (T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
69900 (COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
70000 (SETQ S1 (CDR S1))
70100 (COND (S1 (GO A)))
70200 (RETURN X)))
70300 EXPR)
70400
70500 (DEFPROP DEM
70600 (LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
70700 EXPR)
70800
70900 (DEFPROP DEPTH
71000 (LAMBDA(Z)
71100 (PROG (Z1 Z2)
71200 (SETQ Z1 0)
71300 D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
71400 (SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
71500 (SETQ Z (CDR Z))
71600 (COND (Z (GO D1)))
71700 (RETURN Z1)))
71800 EXPR)
71900
72000 (DEFPROP DEPTH
72100 (NIL . 10)
72200 VALUE)
72300
72400 (DEFPROP DEPTH1
72500 (LAMBDA(Z)
72600 (PROG (Z1)
72700 (SETQ Z1 0)
72800 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
72900 (SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
73000 D2 (SETQ Z (CDR Z))
73100 (COND (Z (GO D1)))
73200 (RETURN Z1)))
73300 EXPR)
73400
73500 (DEFPROP DEL
73600 (LAMBDA (C) (RPLACA (CAR C) NIL))
73700 EXPR)
73800
73900 (DEFPROP DOML
74000 (LAMBDA NIL (TERMS1 (COND ((NEG (CAR L)) (CDDAR L)) (T (CDAR L))) 100))
74100 EXPR)
74200
74300 (DEFPROP DOMC
74400 (LAMBDA NIL (CDR C))
74500 EXPR)
74600
74700 (DEFPROP DOWN
74800 (LAMBDA(N L)
74900 (PROG NIL
75000 (COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
75100 D1 (SETQ N (SUB1 N))
75200 (COND ((ZEROP N) (RETURN L)))
75300 (SETQ L (CDR L))
75400 (COND (L (GO D1)))
75500 (RETURN NIL)))
75600 EXPR)
75700
75800 (DEFPROP EDIT
75900 (LAMBDA(U Z)
76000 (PROG (RES1 U1 U4)
76100 ED4 (COND ((NULL Z) (RETURN RES1)))
76200 (SETQ U4 (CAR Z))
76300 (COND ((EDITSTRAT U4) (GO ED2)))
76400 (SETQ U1 SUBCLAUSES)
76500 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
76600 ED6 (SETQ U1 (CDR U1))
76700 (COND (U1 (GO ED1)))
76800 (SETQ U1 (CDR Z))
76900 (COND ((NULL U1) (GO ED5)))
77000 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
77100 ED7 (SETQ U1 (CDR U1))
77200 (COND (U1 (GO ED3)))
77300 ED5 (SETQ RES1 (CONS U4 RES1))
77400 ED2 (SETQ Z (CDR Z))
77500 (GO ED4)))
77600 EXPR)
77700
77800 (DEFPROP ERPRINT
77900 (LAMBDA (X) (COND (DEBUG (PRINT X))))
78000 EXPR)
78100
78200 (DEFPROP ERPRIN1
78300 (LAMBDA (X) (COND (DEBUG (PRIN1 X))))
78400 EXPR)
78500
78600 (DEFPROP EXPUNGE
78700 (LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
78800 EXPR)
78900
79000 (DEFPROP FINI
79100 (LAMBDA(U R Z1 Z2 E)
79200 (PROG (Z)
79300 (COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
79400 (COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
79500 (SETQ COUNT (PLUS COUNT (LENGTH R)))
79600 (SETQ R (EDIT U R))
79700 (CLAUSES2 R)
79800 (COND ((NULL R) (RETURN 0)))
79900 (BAKSUB CLAUSES R)
80000 (BOOKEEP E R (CONS Z1 Z2))
80100 (SETQ Z (UNITPN R))
80200 (SETQ UNAXP (APPEND (CAR Z) UNAXP))
80300 (SETQ UNAXN (APPEND (CDR Z) UNAXN))
80400 (RETURN (LENGTH R))))
80500 EXPR)
80600
80700 (DEFPROP FIRSTS
80800 (LAMBDA(L)
80900 (PROG (Z)
81000 F (COND ((ATOM (CAR L)) (SETQ Z (CONS (CAR L) Z))) (T (SETQ Z (CONS (CAAR L) Z))))
81100 (SETQ L (CDR L))
81200 (COND (L (GO F)))
81300 (RETURN (REVERSE Z))))
81400 EXPR)
81500
81600 (DEFPROP FIXNEG
81700 (LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
81800 EXPR)
81900
82000 (DEFPROP FIXQFF
82100 (LAMBDA(C)
82200 (PROG (Z)
82300 (SETQ Z (FIXQFF1 C NIL NIL NIL))
82400 (COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
82500 EXPR)
82600
82700 (DEFPROP FIXQFF1
82800 (LAMBDA(C NEW FA TE)
82900 (PROG (Z)
83000 (COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
83100 ((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
83200 ((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
83300 ((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
83400 ((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
83500 (RETURN
83600 (FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
83700 (SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
83800 A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
83900 ((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
84000 (SETQ NEW (CONS (CAR Z) NEW))
84100 B (SETQ Z (CDR Z))
84200 (GO A)))
84300 EXPR)
84400
84500 (DEFPROP GENSKOLEM
84600 (LAMBDA(VARL UNL)
84700 (PROG (Z)
84800 A (COND ((NULL VARL) (RETURN Z)))
84900 (SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
85000 (SETQ VARL (CDR VARL))
85100 (GO A)))
85200 EXPR)
85300
85400 (DEFPROP GETNAME
85500 (LAMBDA(X L)
85600 (PROG (Z)
85700 (SETQ Z (ASSOC X L))
85800 (COND (Z (RETURN (CDR Z))))
85900 (PRINT X)
86000 (PRINC (QUOTE IS-AN-UNBOUND-NAME))
86100 (RETURN NIL)))
86200 EXPR)
86300
86400 (DEFPROP GETVARS
86500 (LAMBDA(C)
86600 (PROG (Z)
86700 A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
86800 ((CONST (CAR C)) NIL)
86900 (T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
87000 (SETQ C (CDR C))
87100 (COND (C (GO A)))
87200 (RETURN Z)))
87300 EXPR)
87400
87500 (DEFPROP GOLIST
87600 (NIL (EO . UEO1)
87700 (DS . UDS1)
87800 (CH . UCH1)
87900 (SY . USY1)
88000 (CU . UCU1)
88100 (FL . UFL1)
88200 (DI . UDI1)
88300 (ST . UST1)
88400 (HA . UST1)
88500 (DE . UDE1)
88600 (IN . UIN1)
88700 (EV . UEV1)
88800 (QU . UQU1)
88900 (TR . UTR1)
89000 (UP . UUP1)
89100 (ME . UME1)
89200 (SI . USI1)
89300 (SE . USE1)
89400 (DO . UDO1)
89500 (CL . UCL1)
89600 (SU . USU1)
89700 (AN . UAN1)
89800 (TE . UTE1)
89900 (RE . URE1)
90000 (SA . USA1)
90100 (PA . UPA1)
90200 (AS . UAS1)
90300 (ED . UED1)
90400 (US . UUS1)
90500 (PR . UPR1)
90600 (FU . UFL2)
90700 (FD . UFL3)
90800 (GO . UGO1)
90900 (EX . UEX1)
91000 (AB . UAB1)
91100 (HE . UHE1))
91200 VALUE)
91300
91400 (DEFPROP GOLIST1
91500 (NIL (AS . AS1) (AT . AT1) (LE . EX1) (SA . S1) (CL . C1) (EX . EXP1) (UP . UPDAT))
91600 VALUE)
91700
91800 (DEFPROP INCLAUSES
91900 (LAMBDA NIL
92000 (PROG (Z AXNO)
92100 (SETQ AXNO (QUOTE AXIOM))
92200 A (SCANSET)
92300 (START)
92400 (SETQ ZIN (ERRSET (<INPUT>) T))
92500 (SCANRESET)
92600 (COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
92700 (SETQ ZIN (TOP))
92800 (COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z)) ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A)))
92900 (OUT >S< ZIN)
93000 (SETQ Z
93100 (APPEND Z
93200 (SETUP
93300 (CNF
93400 (COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
93500 (GO A)))
93600 EXPR)
93700
93800 (DEFPROP INITIAL
93900 (LAMBDA(L)
94000 (PROG (ST Z Z1 Z2)
94100 A (SETQ Z (CDR (ANCESTOR (CAR L))))
94200 (COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
94300 ((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
94400 (T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
94500 (SETQ Z2 (CONS (CAR L) Z2))
94600 (SETQ L (CDR L))
94700 (COND (L (GO A)))
94800 (RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
94900 EXPR)
95000
95100 (DEFPROP INITIALAX
95200 (LAMBDA(L)
95300 (PROG (Z Z1 Z2 Z3 AXNO)
95400 (SETQ AXNO (CAR L))
95500 (SETQ L (CDR L))
95600 A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
95700 (SETQ Z1 (ANCESTOR (CAR L)))
95800 (COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
95900 (SETQ Z2 (ANCESTOR Z))
96000 (RPLACA Z2 Z1)
96100 (RPLACD Z2 AXNO)
96200 (SETQ Z3 (CONS Z Z3))
96300 B (SETQ L (CDR L))
96400 (COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
96500 (GO A)))
96600 EXPR)
96700
96800 (DEFPROP INITIALAX1
96900 (LAMBDA(L1)
97000 (PROG (Z L2 L)
97100 (SETQ L L1)
97200 B1 (SETQ L2 L)
97300 A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
97400 (SETQ L2 (CDR L2))
97500 (COND (L2 (GO A1)))
97600 (SETQ L (CDR L))
97700 (COND (L (GO B1)))
97800 (SETQ L L1)
97900 B (SETQ Z (CDDAAR L))
98000 (COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
98100 ((NUMBERP (CAAAR L)) NIL)
98200 (T (RPLACA (CAAR L) (CAAAAR L))))
98300 (COND ((ATOM (CDDR Z)) (GO A)))
98400 (RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
98500 A (SETQ L (CDR L))
98600 (COND (L (GO B)))
98700 (RETURN L1)))
98800 EXPR)
98900
99000 (DEFPROP MAPIT
99100 (LAMBDA(X XYZ N)
99200 (PROG (Z Z1 Z2)
99300 (SETQ Z (GETNAME X N))
99400 (COND ((NULL Z) (RETURN NIL)))
99500 A (SETQ ZIN (CAR Z))
99600 (SETQ Z2 (ERRSET (XYZ ZIN) T))
99700 (COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
99800 ((NULL (CAR Z2)) NIL)
99900 (T (SETQ Z1 (CONS (CAR Z) Z1))))
00100 (SETQ Z (CDR Z))
00200 (COND (Z (GO A)))
00300 (RETURN (REVERSE Z1))))
00400 EXPR)
00500
00600 (DEFPROP MATCHER
00700 (LAMBDA(L)
00800 (PROG (FLG Z Z1)
00900 (SETQ Z (EVAL (CADR L)))
01000 (SETQ Z1 (CAR L))
01100 (COND ((ATOM (CADR L))
01200 (COND ((MEMQ (CADR L) (QUOTE (T1 T2 T3 T4))) (SETQ FLG 4))
01300 ((MEMQ (CADR L) (QUOTE (L1 L2 L3 L4))) (SETQ FLG 3))
01400 ((MEMQ (CADR L) (QUOTE (C))) (SETQ FLG 2) (SETQ Z (CDR Z)))
01500 (T (ERR NIL))))
01600 ((EQ (CAADR L) (QUOTE TREE)) (SETQ FLG 1))
01700 (T (ERR NIL)))
01800 (COND ((ATOM Z1) (RETURN (MATCH1 Z1 Z FLG)))
01900 ((EQ (CAR Z1) (QUOTE AND)) (GO MAA1))
02000 ((EQ (CAR Z1) (QUOTE OR)) (GO MAO1))
02100 (T (RETURN (MATCH1 Z1 Z FLG))))
02200 MAA1 (SETQ Z1 (CDR Z1))
02300 MAAND
02400 (COND ((NULL Z1) (RETURN T)) ((MATCH1 (CAR Z1) Z FLG) (GO MAA1)) (T (RETURN NIL)))
02500 MAO1 (SETQ Z1 (CDR Z1))
02600 MAOR (COND ((NULL Z1) (RETURN NIL)) ((MATCH1 (CAR Z1) Z FLG) (RETURN T)))
02700 (GO MAO1)))
02800 FEXPR)
02900
03000 (DEFPROP MATCH1
03100 (LAMBDA(X Y FL)
03200 (COND ((ATOM X)
03300 (COND ((EQ X (QUOTE %NG)) (COND ((ISLIT FL) (NEG Y)) ((ISCL FL) (MATCHPN Y T)) (T (ERR NIL))))
03400 ((EQ X (QUOTE %PL)) (COND ((ISLIT FL) (NOT (NEG Y))) ((ISCL FL) (MATCHPN Y NIL)) (T (ERR NIL))))
03500 ((NUMBERP X) (COND ((ISCLS FL) (MATCHTR X Y)) (T (MATMLT X FL))))
03600 ((AND (MEMQ X (QUOTE (C1 C2))) (ISCLS FL)) (MEMQ (EVAL X) Y))
03700 (T (ERR NIL))))
03800 ((NUMBERP (CAR X)) (COND ((ISCLS FL) (MATCHTR (CAR X) Y)) (T (MATMLT (CAR X) Y FL))))
03900 ((EQ (LENGTH X) 1) (MATMLT (CAR X) Y FL))
04000 ((ISCLS FL) NIL)
04100 (T (MATMLT* X Y FL))))
04200 EXPR)
04300
04400 (DEFPROP MATCHTR
04500 (LAMBDA (N TR) (MEMQ (CAR (DOWN N CLAUSES)) TR))
04600 EXPR)
04700
04800 (DEFPROP MATCHPN
04900 (LAMBDA(X FL)
05000 (PROG (Z)
05100 A (SETQ Z (NEG (CAR X)))
05200 (COND ((AND Z FL) (RETURN T)) ((AND (NOT Z) (NOT FL)) (RETURN T)))
05300 (SETQ X (CDR X))
05400 (COND (X (GO A)))
05500 (RETURN NIL)))
05600 EXPR)
05700
05800 (DEFPROP MATMLT
05900 (LAMBDA(X Y FL)
06000 (PROG NIL
06100 (COND ((AND (ISTRM FL) (NOT (ASSOC X TBL))) (ERR NIL))
06200 ((ISTRM FL) (RETURN (OCR X Y)))
06300 ((ISLIT FL) (RETURN (COND ((NEG Y) (OCR X (CDR Y))) (T (OCR X Y))))))
06400 A (COND ((COND ((NEG (CAR Y)) (OCR X (CDAR Y))) (T (OCR X (CAR Y)))) (RETURN T)))
06500 (SETQ Y (CDR Y))
06600 (COND (Y (GO A)))
06700 (RETURN NIL)))
06800 EXPR)
06900
07000 (DEFPROP MATMLT*
07100 (LAMBDA(X Y FL)
07200 (PROG (Z)
07300 (COND ((AND (ISTRM FL) (NOT (ASSOC (CAR X) TBL))) (ERR NIL))
07400 ((EQ (CAR X) (QUOTE %NG)) (SETQ X (CDR X)) (GO M1))
07500 ((NOT (ISCL FL)) (SETQ Y (LIST Y))))
07600 D (SETQ X (VARIT (LIST X)))
07700 B (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
07800 A (COND ((UNI X (CAR Z) NIL) (RETURN T)))
07900 (SETQ Z (CDR Z))
08000 (COND (Z (GO A)))
08100 (SETQ Y (CDR Y))
08200 (COND (Y (GO B)))
08300 (RETURN NIL)
08400 M1 (COND ((NEG (CAR Y)) (GO M2)))
08500 M3 (SETQ Y (CDR Y))
08600 (COND (Y (GO M1)))
08700 (RETURN NIL)
08800 M2 (COND ((EQ (LENGTH X) 1) (COND ((EQ (CADAR Y) (CAR X)) (RETURN T)) (T (GO M3)))) (T (GO D)))))
08900 EXPR)
09000
09100 (DEFPROP MAX
09200 (LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
09300 EXPR)
09400
09500 (DEFPROP MEMC
09600 (LAMBDA(C L)
09700 (PROG NIL
09800 (COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
09900 B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
10000 (SETQ L (CDR L))
10100 (COND (L (GO B)))
10200 (RETURN NIL)
10300 A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
10400 (SETQ L (CDR L))
10500 (COND (L (GO A)))
10600 (RETURN NIL)))
10700 EXPR)
10800
10900 (DEFPROP MIN1
11000 (LAMBDA(L)
11100 (PROG (Z Z1)
11200 (SETQ Z (CAR L))
11300 M1 (SETQ Z1 (CDR L))
11400 (COND ((NULL Z1)
11500 (COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
11600 ((NUMBERP (CAAR Z1)) (GO M2))
11700 ((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
11800 M2 (SETQ L (CDR L))
11900 (GO M1)))
12000 EXPR)
12100
12200 (DEFPROP MINIMIZE
12300 (LAMBDA(Z3)
12400 (PROG (Z1 Z2 Z4)
12500 (SETQ Z2 (LIST (CAR Z3)))
12600 ED2 (SETQ Z3 (CDR Z3))
12700 (COND ((NULL Z3) (RETURN (REVERSE Z2))))
12800 (SETQ Z4 (CAR Z3))
12900 (SETQ Z1 Z2)
13000 ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
13100 (SETQ Z1 (CDR Z1))
13200 (COND (Z1 (GO ED1)))
13300 (SETQ Z1 (CDR Z3))
13400 ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
13500 (SETQ Z1 (CDR Z1))
13600 (GO ED4)
13700 ED5 (SETQ Z2 (CONS Z4 Z2))
13800 (GO ED2)))
13900 EXPR)
14000
14100 (DEFPROP MIN
14200 (LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
14300 EXPR)
14400
14500 (DEFPROP MKSYM
14600 (LAMBDA NIL
14700 (PROG NIL
14800 (SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
14900 (SETQ PREFN (CONS (CAR FNLIST) PREFN))
15000 (RETURN (CAR FNLIST))))
15100 EXPR)
15200
15300 (DEFPROP MODEL
15400 (LAMBDA(C)
15500 (PROG (Z)
15600 (SETQ Z (CDR C))
15700 M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
15800 M2 (SETQ Z (CDR Z))
15900 (COND (Z (GO M1)))
16000 (RETURN NIL)
16100 M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
16200 (GO M2)))
16300 EXPR)
16400
16500 (DEFPROP NCONC1
16600 (LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
16700 EXPR)
16800
16900 (DEFPROP NEGATE
17000 (LAMBDA(Z)
17100 (PROG (BDY)
17200 A (SETQ Z (CDR Z))
17300 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
17400 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
17500 (SETQ Z (CDDR Z))
17600 C (COND ((NULL Z) (GO D)))
17700 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
17800 (SETQ Z (CDR Z))
17900 (GO C)
18000 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
18100 EXPR)
18200
18300 (DEFPROP NEGSGN
18400 (NIL . ¬)
18500 VALUE)
18600
18700 (DEFPROP NOSYM
18800 (LAMBDA (L) (COND ((NULL L) 0) ((ATOM L) 1) (T (MAX (ADD1 (NOSYM (CAR L))) (NOSYM (CDR L))))))
18900 EXPR)
19000
19100 (DEFPROP OCR
19200 (LAMBDA (X Y) (OCR1 X (LIST Y)))
19300 EXPR)
19400
19500 (DEFPROP OCR1
19600 (LAMBDA(X Y)
19700 (COND ((NULL Y) NIL)
19800 ((VAR (CAR Y)) (OCR1 X (CDR Y)))
19900 ((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR1 X (CDR Y)))))
20000 ((EQ X (CAAR Y)) T)
20100 ((OCR1 X (CDAR Y)) T)
20200 (T (OCR1 X (CDR Y)))))
20300 EXPR)
20400
20500 (DEFPROP ONEGSGN
20600 (NIL . ¬)
20700 VALUE)
20800
20900 (DEFPROP *NOPOINT
21000 (NIL . T)
21100 VALUE)
21200
21300 (DEFPROP OCCUR
21400 (LAMBDA(X Z)
21500 (PROG (Z1)
21600 OC1 (SETQ Z1 (CAR Z))
21700 (COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
21800 ((CONST Z1) (GO OC2))
21900 ((OCCUR X (CDR Z1)) (RETURN T)))
22000 OC2 (SETQ Z (CDR Z))
22100 (COND (Z (GO OC1)))
22200 (RETURN NIL)))
22300 EXPR)
22400
22500 (DEFPROP ORDER
22600 (LAMBDA(X Y)
22700 (COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
22800 ((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
22900 EXPR)
23000
23100 (DEFPROP ORDEREQUAL
23200 (LAMBDA(S)
23300 (PROG NIL
23400 (COND ((VAR (CAR S))
23500 (COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
23600 ((CONST (CAR S))
23700 (COND ((VAR (CADR S)) (RETURN NIL))
23800 ((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
23900 (T (GO A))))
24000 ((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
24100 ((GREATERP (DEPTH1 (CDAR S)) (DEPTH1 (CDADR S))) (RETURN NIL)))
24200 A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
24300 EXPR)
24400
24500 (DEFPROP PARMOD
24600 (LAMBDA(C D)
24700 (COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
24800 EXPR)
24900
25000 (DEFPROP PARMOD1
25100 (LAMBDA(C D)
25200 (PROG (YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
25300 (COND ((EQ C D) (RETURN NIL)))
25400 (SETQ YC (CDR C))
25500 PAR1 (SETQ YD (CDR D))
25600 (SETQ X (CAR YC))
25700 (COND ((NEG X) (RETURN PAR))
25800 ((ORDERP (CAR X) EQUAL) (GO PAR2))
25900 ((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
26000 PAR3 PAR3A
26100 (COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
26200 (SETQ Y1 (CDR X))
26300 (COND ((VAR (CAR Y1)) (GO PAR7A)))
26400 (SETQ Y2 (CADR Y1))
26500 (SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
26600 (COND ((NULL Z) (GO PAR7A)))
26700 PAR5 (SETQ Z1 Z)
26800 PAR4 (SETQ Y (UNIFY (LIST (CAR Y1)) (LIST (CAAR Z1))))
26900 (COND (Y (GO PAR6)))
27000 PAR7 (SETQ Z1 (CDR Z1))
27100 (COND (Z1 (GO PAR4)))
27200 PAR7A
27300 (SETQ YD (CDR YD))
27400 (COND (YD (GO PAR3A)))
27500 PAR2 (SETQ YC (CDR YC))
27600 (COND (YC (GO PAR1)))
27700 (RETURN PAR)
27800 PAR6 (SETQ TS (CADR (SUBS3T* (CDR Y) (LIST NIL Y2))))
27900 PAR9 (SETQ PARRES (SUBS3TA (CDR Y) Z2 (CAR Z1) TS))
28000 (COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
28100 (SETQ Y (UNION (CDR Y) C D X (CAR YD)))
28200 (COND ((NULL Y) (GO PAR7)))
28300 (SETQ PAR (CONS (SET2 (CAR (COND (DLIST (DEMOD Y DLIST)) (T Y))) TBL) PAR))
28400 (GO PAR7)))
28500 EXPR)
28600
28700 (DEFPROP POTZ
28800 (LAMBDA(X)
28900 (PROG (Z Z1)
29000 (SETQ Z (POTZ1 X))
29100 (COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
29200 (SETQ POTZTBL (CONS Z POTZTBL))
29300 (RETURN Z)))
29400 EXPR)
29500
29600 (DEFPROP PRECNF
29700 (LAMBDA(X)
29800 (COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
29900 ((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
30000 ((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
30100 ((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
30200 ((EQ (CAR X) (QUOTE EQUIV))
30300 (LIST (QUOTE AND)
30400 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
30500 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
30600 (T X)))
30700 EXPR)
30800
30900 (DEFPROP PROOF1
31000 (LAMBDA(L)
31100 (PROG (Q X Y Z P P1)
31200 (PRINC (QUOTE / ))
31300 (PRINC (QUOTE / ))
31400 (PRFPRINT (CDR L))
31500 (SETQ P (ANCESTOR L))
31600 (COND ((ATOM (CDR P)) (GO P3)))
31700 (SETQ P1 (CDR P))
31800 (SETQ P (CAR P))
31900 (PRINC (QUOTE / ))
32000 (PRINC 1)
32100 (PRINC (QUOTE / ))
32200 (PRINC 2)
32300 (SETQ X 1)
32400 (SETQ Y 2)
32500 (SETQ Q (LIST (CONS X P) (CONS Y P1)))
32600 P1 (SETQ Z (ANCESTOR (CDAR Q)))
32700 (COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
32800 (SETQ X (ADD1 Y))
32900 (SETQ Y (ADD1 X))
33000 (PRINT (CAAR Q))
33100 (PRFPRINT (CDDAR Q))
33200 (PRINC X)
33300 (PRINC (QUOTE / ))
33400 (PRINC Y)
33500 (SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
33600 P2 (SETQ Q (CDR Q))
33700 (COND ((NULL Q) (RETURN NIL)))
33800 (GO P1)
33900 P3 (PRIN1 (CDR P))
34000 (RETURN (TERPRI))))
34100 EXPR)
34200
34300 (DEFPROP PROVE
34400 (LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
34500 FEXPR)
34600
34700 (DEFPROP PRPAR
34800 (LAMBDA(L)
34900 (PROG NIL
35000 (CLAUSES CLAUSES)
35100 (TERPRI)
35200 P1 (PROOF1 (CAR L))
35300 (TERPRI)
35400 (TERPRI)
35500 (SETQ L (CDR L))
35600 (COND (L (GO P1)))
35700 (RETURN NIL)))
35800 EXPR)
35900
36000 (DEFPROP PRFPRINT
36100 (LAMBDA(X)
36200 (PROG NIL
36300 (SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
36400 (SETQ LAST NIL)
36500 (FPRINT &&Z 0)))
36600 EXPR)
36700
36800 (DEFPROP PRFPR1
36900 (LAMBDA(L)
37000 (PROG (Z)
37100 (COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
37200 (PRINC (CAR L))
37300 (SETQ L (CDR L))
37400 (PRINC (QUOTE /())
37500 P1 (COND ((VAR (CAR L))
37600 (COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
37700 (T (PRINC (QUOTE X))
37800 (COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
37900 (T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
38000 ((CONST (CAR L)) (PRINC (CAAR L)))
38100 (T (PRFPR1 (CAR L))))
38200 P2 (SETQ L (CDR L))
38300 (COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
38400 (PRINC (QUOTE /,))
38500 (GO P1)))
38600 EXPR)
38700
38800 (DEFPROP PROOF
38900 (LAMBDA(L R)
39000 (PROG (Q Q1 X Z)
39100 (SETQ LHP L)
39200 (SETQ RHP R)
39300 (RPLACA (MKWRD L) 1)
39400 (RPLACA (MKWRD R) 2)
39500 (SETQ X 2)
39600 (SETQ Q (LIST L R))
39700 (SETQ Q1 Q)
39800 P1 (SETQ Z (ANCESTOR (CAR Q)))
39900 (COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
40000 (RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
40100 (RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
40200 (NCONC Q (LIST (CAR Z) (CDR Z)))
40300 P2 (SETQ Q (CDR Q))
40400 (COND (Q (GO P1)))
40500 (PRINT (QUOTE NIL))
40600 (PRINC (CAR (MKWRD (CAR Q1))))
40700 (PRINC (QUOTE / ))
40800 (PRINC (CAR (MKWRD (CADR Q1))))
40900 (SETQ X 1)
41000 A (COND
41100 ((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
41200 (PRFPRINT (CDAR Q1))
41300 (COND
41400 ((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
41500 ((ATOM (CDR (ANCESTOR (CAR Q1))))
41600 (PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
41700 (PRINC (QUOTE / ))
41800 (PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
41900 (T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
42000 (PRINC (QUOTE / ))
42100 (PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
42200 (SETQ Q1 (CDR Q1))
42300 (SETQ X (ADD1 X))
42400 (COND (Q1 (GO A)))))
42500 EXPR)
42600
42700 (DEFPROP PTRS
42800 (LAMBDA(X)
42900 (PROG (Z)
43000 A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
43100 (SETQ X (CDR X))
43200 (COND (X (GO A)))
43300 (RETURN Z)))
43400 EXPR)
43500
43600 (DEFPROP QUERY
43700 (LAMBDA NIL
43800 (PROG NIL
43900 (COND (STRATEGY (PRINT (QUOTE CHOICE-STRATEGY-IS:)) (OUT >ST< (CAR (LAST STRATEGY)))))
44000 (PRINT (QUOTE EDIT-STRATEGY-IS:))
44100 (OUT >ST< (CAR (LAST EDITSTRAT)))
44200 (COND ((AND (NULL PMODEL) (NULL NMODEL)) (GRINDEF MODEL))
44300 (T (PRINT (QUOTE POSITIVE-MODEL=))
44400 (PRINC PMODEL)
44500 (PRINT (QUOTE NEGATIVE-MODEL=))
44600 (PRINC NMODEL)))
44700 (PRINT (QUOTE PARMODULATE))
44800 (PRINC (QUOTE =))
44900 (COND ((NOT PFLG) (PRINC T)
45000 (PRINT (QUOTE EQUAL-SYMBOL))
45100 (PRINC (QUOTE =))
45200 (PRINC EQUAL)
45300 (PRINT (QUOTE PAR-DEPTH-BOUND))
45400 (PRINC (QUOTE =))
45500 (PRINC PDEPTH))
45600 (T (PRINC NIL)))
45700 (PRINT (QUOTE ELAPSED-TIME))
45800 (PRINC (QUOTE =))
45900 (PRINC (TIMEIT))
46000 (RETURN (TERPRI))))
46100 EXPR)
46200
46300 (DEFPROP REAL-LNGTH
46400 (LAMBDA(L)
46500 (PROG (N)
46600 (SETQ N 0)
46700 A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
46800 (SETQ L (CDR L))
46900 (GO A)))
47000 EXPR)
47100
47200 (DEFPROP REDUCER
47300 (LAMBDA(C L)
47400 (PROG (Z Z1 Z2 Z3 C1)
47500 (SETQ Z (CDAR C))
47600 (SETQ Z2 (CDAAR C))
47700 (SETQ C1 C)
47800 (SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
47900 A (COND ((EQ L (CDR C1)) (GO B)))
48000 (SETQ C1 (CDR C1))
48100 (SETQ Z1 (CDR Z1))
48200 (GO A)
48300 B (RPLACD C1 (CDDR C1))
48400 (COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
48500 (COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
48600 (RPLACD Z1 (CDDR Z1))
48700 (RPLACA Z2 (CDR Z3))
48800 (RPLACA (CAAR C) (SUB1 (CAAAR C)))
48900 (RETURN C)))
49000 EXPR)
49100
49200 (DEFPROP REENTER
49300 (LAMBDA NIL (PROG NIL (ATTEMPT1 XYZ2) (RETURN NIL)))
49400 EXPR)
49500
49600 (DEFPROP RESTORE
49700 (LAMBDA(IL)
49800 (PROG (ZZ) (EVAL (CONS (QUOTE INPUT) IL)) (INC T) (SETQ ZZ (RESTORE1 (READ))) (INC NIL) (RETURN (SET3 ZZ))))
49900 FEXPR)
50000
50100 (DEFPROP RESTORE1
50200 (LAMBDA(L)
50300 (PROG (Z2 Z L1 L2 Z1 N)
50400 (SETQ L1 L)
50500 (SETQ N 0)
50600 D (SETQ L2 (CONS (CONS N (CAR L)) L2))
50700 (SETQ L (CDR L))
50800 (SETQ N (ADD1 N))
50900 (COND (L (GO D)))
51000 (SETQ L L1)
51100 E (SETQ Z (CAAR L1))
51200 (SETQ Z1 (CADR Z))
51300 (COND ((NULL Z1) (GO A)))
51400 (SETQ Z2 (CDAR L1))
51500 B (COND ((ZEROP Z1) (RPLACA (CDR Z) Z2) (GO A)))
51600 (SETQ Z1 (SUB1 Z1))
51700 (SETQ Z2 (CDR Z2))
51800 (GO B)
51900 A (SETQ Z1 (CDDDR Z))
52000 (COND ((NULL (CDR Z1)) (RPLACD (CDDR Z) (CAR Z1)) (GO C)) ((NULL (CAR Z1)) (SETQ Z1 (CDR Z1))))
52100 F (RPLACA Z1 (CDR (ASSOC (CAR Z1) L2)))
52200 (RPLACD Z1 (CDR (ASSOC (CDR Z1) L2)))
52300 C (SETQ L1 (CDR L1))
52400 (COND (L1 (GO E)))
52500 (RETURN L)))
52600 EXPR)
52700
52800 (DEFPROP RESOLVE
52900 (LAMBDA(C D)
53000 (COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
53100 ((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
53200 (T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
53300 EXPR)
53400
53500 (DEFPROP RESTS
53600 (LAMBDA(L)
53700 (PROG (Z Z1)
53800 A (COND ((ATOM (CAR L)) (SETQ Z (CONS (CAR L) Z)))
53900 ((EQ (LENGTH (CAR L)) 1) (RETURN NIL))
54000 (T (SETQ Z1 T) (SETQ Z (CONS (CDAR L) Z))))
54100 (SETQ L (CDR L))
54200 (COND (L (GO A)) ((NULL Z1) (RETURN NIL)))
54300 (RETURN (REVERSE Z))))
54400 EXPR)
54500
54600 (DEFPROP RESOLVE1
54700 (LAMBDA(C D)
54800 (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
54900 (COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
55000 (SETQ YC (CDR C))
55100 (SETQ CB (POSBIT C))
55200 (SETQ YD1 (NEGL D))
55300 (SETQ DB1 (NEGBIT D))
55400 (SETQ DB DB1)
55500 (SETQ YD YD1)
55600 RES1 (SETQ X (CAR YC))
55700 (COND ((NEG X) (RETURN RES)))
55800 (SETQ Y (CAR YD))
55900 (COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
56000 (SETQ YD1 YD)
56100 (SETQ DB1 DB)
56200 (GO RES2A)
56300 RES2 (SETQ Y (CAR YD))
56400 (COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
56500 RES2A
56600 (COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
56700 (SETQ Z (UNIFY (CDR X) (CDDR Y)))
56800 (COND ((NULL Z) (GO RES2B)))
56900 (SETQ PARRES NIL)
57000 (SETQ Z (UNION (CDR Z) C D X Y))
57100 (COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
57200 (SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST)) (T Z))) TBL) RES))
57300 RES2B
57400 (SETQ YD (CDR YD))
57500 (COND (YD (SETQ DB (CDR DB)) (GO RES2)))
57600 RES3A
57700 (SETQ DB DB1)
57800 (SETQ YD YD1)
57900 RES3 (SETQ YC (CDR YC))
58000 (COND (YC (SETQ CB (CDR CB)) (GO RES1)))
58100 (RETURN RES)
58200 RES4 (SETQ YD (CDR YD))
58300 (COND (YD (SETQ DB (CDR DB)) (GO RES1)))
58400 (GO RES3A)))
58500 EXPR)
58600
58700 (DEFPROP RESTART
58800 (LAMBDA(X)
58900 (PROG (ZZ TIME1)
59000 (EVAL (CONS (QUOTE INPUT) X))
59100 (INC T)
59200 (SETQ ZZ (RESTORE1 (READ)))
59300 (SETQ STRAT (READ))
59400 (SETQ COND (READ))
59500 (INC NIL)
59600 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
59700 (RETURN (ATTEMPT (CONS ZZ (FIXSET ZZ)) STRAT COND))))
59800 FEXPR)
59900
60000 (DEFPROP RESET
60100 (LAMBDA(L)
60200 (PROG (Z) R1 (SETQ Z (EVAL (CONS (QUOTE RESET1) (CAR L)))) (SETQ L (CDR L)) (COND (L (GO R1))) (RETURN Z)))
60300 FEXPR)
60400
60800
60900 (DEFPROP RESET1
61000 (LAMBDA(L)
61100 (PROG (X Z2 Z3 ZZ XX Z Z1 F1)
61200 (SETQ Z STATEVECTOR)
61300 A (COND
61400 ((EQ (CAR L) (CAR Z)) (SETQ F1 T)
61500 (COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
61600 (T (SET (CAR Z) (EVAL (CADR L)))))))
61700 R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
61800 (SETQ Z (CDR Z))
61900 (COND (Z (GO A)))
62000 (COND (F1 (RETURN (REVERSE Z1))))
62100 R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
62200 (PRINC (CAR L))
62300 (TERPRI)
62400 (ERR NIL)
62500 R1 (SETQ X (QUOTE (X)))
62600 (SETQ L (CDR L))
62700 R4 (SETQ Z2 (CAR L))
62800 (COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
62900 SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
63000 ((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
63100 (PROG (ZZ)
63200 (GO B)
63300 A (SETQ ZZ (CONS (CDAR XX) ZZ))
63400 (SETQ XX (CDR XX))
63500 B (COND (XX (GO A)))
63600 (SETQ SUPPORT ZZ))
63700 (SETQ ZZ (QUOTE (SUPPORT C2))))
63800 ((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
63900 (SETQ NMODEL (CADDAR L))
64000 (SETQ ZZ (CONS (CONS Z3 X) ZZ)))
64100 ((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
64200 ((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
64300 ((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
64400 (T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
64500 (SETQ L (CDR L))
64600 (COND (L (GO R4)))
64700 (COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
64800 (GO R2)))
64900 FEXPR)
65000
65100 (DEFPROP SAVE
65200 (LAMBDA(CL)
65300 (PROG (L)
65400 (SETQ L (SAVE1 (EVAL (CADDR CL))))
65500 (EVAL (CONS (QUOTE OUTPUT) (LIST (CAR CL) (CADR CL))))
65600 (OUTC T T)
65700 (PRINT L)
65800 (PRINT STRAT)
65900 (PRINT COND)
66000 (OUTC NIL T)
66100 (RETURN NIL)))
66200 FEXPR)
66300
66400 (DEFPROP SAVE1
66500 (LAMBDA(L)
66600 (PROG (L1 N ASLST CLST Z Z2 Z3 Z4 Z5)
66700 (SETQ N 0)
66800 (SETQ Z L)
66900 A (SETQ ASLST (CONS (CONS (CAR L) N) ASLST))
67000 (SETQ L (CDR L))
67100 (SETQ N (ADD1 N))
67200 (COND (L (GO A)))
67300 (SETQ CLST (LAST Z))
67400 (SETQ L Z)
67500 B (SETQ Z2 (CAAR L))
67600 (COND ((NULL (CAR Z2)) (SETQ Z3 NIL)) (T (SETQ Z3 (CAAR Z2))))
67700 (COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
67800 (T
67900 (SETQ Z4
68000 (PROG (Z Z1 N)
68100 (SETQ N 0)
68200 (SETQ Z1 (CDAR L))
68300 (SETQ Z (CADR Z2))
68400 A (COND ((EQ Z Z1) (RETURN N)))
68500 (SETQ Z1 (CDR Z1))
68600 (SETQ N (ADD1 N))
68700 (GO A)))))
68800 (SETQ Z (CDDDR Z2))
68900 (COND ((ATOM (CDR Z))
69000 (COND ((NOT (ATOM (CAR Z))) (SETQ Z5 (UNWIND (CAAR Z) (CDAR Z) CLST ASLST N))
69100 (SETQ N (CDR Z5))
69200 (SETQ Z5 (CONS NIL (CAR Z5))))
69300 (T (SETQ Z5 (LIST Z)))))
69400 (T (SETQ Z2 (UNWIND (CAR Z) (CDR Z) CLST ASLST N)) (SETQ Z5 (CAR Z2)) (SETQ N (CDR Z2))))
69500 (SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
69600 (SETQ L1 (CONS (CONS Z (CDAR L)) L1))
69700 C (SETQ L (CDR L))
69800 (COND (L (GO B)))
69900 (RPLACD CLST NIL)
70000 (RETURN (REVERSE L1))))
70100 EXPR)
70200
70300 (DEFPROP SET1
70400 (LAMBDA(L)
70500 (PROG (TBL N)
70600 (SETQ N 1)
70700 (SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
70800 A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
70900 (SETQ L (CDR L))
71000 (COND (L (SETQ N (ADD1 N)) (GO A)))
71100 (RETURN (SETU TBL))))
71200 EXPR)
71300
71400 (DEFPROP SET2
71500 (LAMBDA(C L)
71600 (PROG (X Z T1 T2 T3* T2* T3 Z1)
71700 (SETQ T2 (SETQ T2* (LIST NIL)))
71800 (SETQ T3 (SETQ T3* (LIST NIL)))
71900 (SETQ X (CDR C))
72000 S1 (SETQ Z (CDAR X))
72100 (SETQ T1 NIL)
72200 (COND ((NEG (CAR X)) (GO S2)))
72300 S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
72400 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
72500 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
72600 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
72700 (SETQ Z (CDR Z))
72800 (COND (Z (GO S1A)))
72900 (SETQ X (CDR X))
73000 (RPLACD T2* (LIST (POTZ T1)))
73100 (SETQ T2* (CDR T2*))
73200 (COND (X (GO S1)))
73300 S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
73400 (RPLACA (CAR C) (CONS (CAAR C) T3))
73500 (RETURN C)
73600 S2 (SETQ Z (CDDAR X))
73700 (SETQ T1 NIL)
73800 S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
73900 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
74000 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
74100 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
74200 (SETQ Z (CDR Z))
74300 (COND (Z (GO S2A)))
74400 (SETQ X (CDR X))
74500 (RPLACD T3* (LIST (POTZ T1)))
74600 (SETQ T3* (CDR T3*))
74700 (COND (X (GO S2)))
74800 (GO S4)))
74900 EXPR)
75000
75100 (DEFPROP SET3
75200 (LAMBDA(Z)
75300 (PROG (E)
75400 (COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
75500 (SETQ E Z)
75600 S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
75700 (SETQ E (CDR E))
75800 (COND (E (GO S1)))
75900 (RETURN Z)))
76000 EXPR)
76100
76200 (DEFPROP SETUP
76300 (LAMBDA(Z)
76400 (PROG (BL Z1 Z2 Z3 Z4 Z5)
76500 SET2 (SETQ Z3 (CAR Z))
76600 (SETQ Z2 0)
76700 (SETQ BL NIL)
76800 (SETQ NO* NO)
76900 (SETQ Z5 NIL)
77000 S1 (SETQ Z4 (MIN1 Z3))
77100 (COND ((NULL Z4) (GO S3)))
77200 (UPIT Z4)
77300 (COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
77400 (SETQ Z2 (ADD1 Z2))
77500 (SETQ Z5 (CONS Z4 Z5))
77600 (GO S1)
77700 S3 (SETQ Z3 NIL)
77800 (SETQ Z4 Z5)
77900 S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
78000 (SETQ Z4 (CDR Z4))
78100 (COND (Z4 (GO S2)))
78200 SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
78300 SET1 (SETQ Z1 (CONS Z5 Z1))
78400 S4 (SETQ Z (CDR Z))
78500 (COND (Z (GO SET2)))
78600 (RETURN Z1)))
78700 EXPR)
78800
78900 (DEFPROP SEARCH2
79000 (LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
79100 EXPR)
79200
79300 (DEFPROP S2
79400 (LAMBDA(X Y Z)
79500 (PROG (Z1)
79600 (SETQ Z1 (CDR Z))
79700 A (COND ((NULL Z1) (RETURN Z))
79800 ((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
79900 ((CONST (CAR Z1)) NIL)
80000 (T (RPLACA Z1 (S2 X Y (CAR Z1)))))
80100 (SETQ Z1 (CDR Z1))
80200 (GO A)))
80300 EXPR)
80400
80500 (DEFPROP SETQUERY
80600 (LAMBDA (X) (SETQUERY2 X NIL NIL))
80700 EXPR)
80800
80900 (DEFPROP SETQUERY1
81000 (LAMBDA(XYZ XYZ1)
81100 (PROG (Z)
81200 (SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
81300 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
81400 (RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
81500 EXPR)
81600
81700 (DEFPROP SETQUERY2
81800 (LAMBDA(XX YY FLG)
81900 (PROG (XYZ1 N
82000 CHAN
82100 Z
82200 Z1
82300 Z3
82400 XYZ
82500 Z6
82600 SUPPORT
82700 EDITSTRAT
82800 MERGE
82900 ORDER
83000 DEBUG
83100 DEPTH
83200 LENGTH
83300 ANCESTRY
83400 STRATEGY
83500 PMODEL
83600 NMODEL
83700 PFLG
83800 EQUAL
83900 PDEPTH
84000 DLIST)
84100 (SETQ CHAN (OUTC NIL NIL))
84200 (COND (FLG (UPDATESTATE YY)))
84300 (SETQ XYZ1 XX)
84400 (COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
84500 (PRINT SETQMESS)
84600 (SETQ XX (UPDATE XX))
84700 (SETQ XYZ1 XX)
84800 SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
84900 (PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
85000 (SETQ N 1)
85100 AA (UP1B (CAR XX) N)
85200 (SETQ N (ADD1 N))
85300 (SETQ XX (CDR XX))
85400 (COND (XX (GO AA)))
85500 SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
85600 (AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
85700 (COND
85800 ((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
85900 SRA2 (PRINT (QUOTE DOIT-CHOICE-STRATEGY))
86000 (SCANSET)
86100 (START)
86200 (SETQ Z (ERRSET (<ST>) T))
86300 (SCANRESET)
86400 (COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SRA2)))
86500 (SETQ ZIN (TOP))
86600 (SETQ STRATEGY (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) ZIN))
86700 (OUT >ST< ZIN)
86800 SRB (PRINT (QUOTE DEBUG))
86900 (PRINC (QUOTE =))
87000 (COND (FLG (RESTRAT DEBUG SRA SRAA) (PRINC DEBUG) (BARF NIL) (RESTRAT2 DEBUG SRA))
87100 (T (RESTRATS DEBUG SRA)))
87200 SRAA SRC
87300 SRD (PRINT (QUOTE DOIT-EDIT-STRATEGY))
87400 (SCANSET)
87500 (START)
87600 (SETQ Z1 (ERRSET (<ST>) T))
87700 (SCANRESET)
87800 (COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
87900 (SETQ ZIN (TOP))
88000 (SETQ EDITSTRAT (LIST (QUOTE LAMBDA) (QUOTE (C)) ZIN))
88100 (OUT >ST< ZIN)
88200 SRCA SRI
88300 (PRINT (QUOTE (UNIT-REDUCTION (Y / N))))
88400 (COND (FLG (RESTRAT UFLG SRD SRIA) (PRINC UFLG) (BARF NIL) (RESTRAT2 UFLG SRC))
88500 (T (RESTRATS UFLG SRD)))
88600 SRIA SRE
88700 (PRINT (QUOTE PARAMODULATE))
88800 (COND (FLG (PRINC (QUOTE IS))
88900 (PRINC (QUOTE / ))
89000 (COND (PFLG (PRINC (QUOTE N))) (T (PRINC (QUOTE Y))))
89100 (PRINT (QUOTE (DO YOU WANT TO PARAMODULATE (Y / N))))
89200 (SETQ Z3 (READ))
89300 (COND ((EQ Z3 (QUOTE Y)) (SETQ PFLG NIL) (GO SRDA))
89400 ((EQ Z3 (QUOTE N)) (GO SPQ5))
89500 ((EQ Z3 ESCAPE) (PRINT (QUOTE RESETTING-TO:)) (GO SRI))
89600 (T (GO SRE))))
89700 (T (PRINC (QUOTE (Y / N)))
89800 (RESTRATS Z3 SRI)
89900 (SETQ EQUAL ESCAPE)
90000 (COND ((EQ Z3 (QUOTE N)) (GO SPQ5)))))
90100 SRDA (SETQ AXNO 1)
90200 SRF (PRINT (QUOTE EQUAL-SYMBOL))
90300 (PRINC (QUOTE =))
90400 (COND (FLG (RESTRAT EQUAL SRE SREA) (PRINC EQUAL) (BARF NIL) (RESTRAT2 EQUAL SRE))
90500 (T (RESTRATS EQUAL SRE)))
90600 SREA (SETQ PFLG NIL)
90700 SRG (PRINT (QUOTE PAR-DEPTH-BOUND))
90800 (PRINC (QUOTE =))
90900 (COND (FLG (RESTRAT PDEPTH SRF SRFA) (PRINC PDEPTH) (BARF NIL) (RESTRAT2 PDEPTH SRF))
91000 (T (RESTRATS PDEPTH SRF)))
91100 SRFA P1
91200 (PRINT (QUOTE DEMODULATION-LIST))
91300 (PRINC (QUOTE =))
91400 (PRINT (QUOTE (TYPE: 'NONE' OR 'IN' (TO INSERT))))
91500 (COND (FLG (RESTRAT XYZ SRH SRHA) (PRINC XYZ) (BARF NIL) (RESTRAT2 XYZ SRH)) (T (RESTRATS XYZ SRG)))
91600 SRHA (SETQ DLIST NIL)
91700 (COND ((EQ XYZ (QUOTE NONE)) (GO SPQ6))
91800 ((EQ XYZ (QUOTE IN)) (GO P2))
91900 (T (PRINT (QUOTE UNDEFINED-SPECIFICATION-FOR-DEMOD-LIST))))
92000 (GO P1)
92100 P2 (SETQ Z3 (INCLAUSES))
92200 P2A (COND ((NULL Z3) (PRINT (QUOTE ERROR-TRY-AGAIN)) (GO P1)))
92300 P3 (SET3 (SETQ DLIST Z3))
92400 SRH (PRINT (QUOTE DEMOD-DEPTH-BOUND=))
92500 (COND (FLG (RESTRAT DDEPTH P1 SRGA) (PRINC DDEPTH) (BARF NIL) (RESTRAT2 DDEPTH P1))
92600 (T (RESTRATS DDEPTH P1)))
92700 SRGA P6
92800 (GO SPQ6)
92900 SPQ5 (SETQ PFLG T)
93000 SPQ6 (SETQ Z1
93100 (LIST STRATEGY
93200 SUPPORT
93300 EDITSTRAT
93400 MERGE
93500 ORDER
93600 DEBUG
93700 DEPTH
93800 LENGTH
93900 ANCESTRY
94000 PMODEL
94100 NMODEL
94200 PFLG
94300 EQUAL
94400 PDEPTH
94500 DLIST))
94600 (OUTC CHAN NIL)
94700 (COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
94800 EXPR)
94900
95000 (DEFPROP SUBS3TA
95100 (LAMBDA(L Z XX TS)
95200 (PROG (X1 X2 X3 Z4)
95300 (SETQ X1 (LIST (CAR Z)))
95400 (SETQ X2 X1)
95500 (GO SUB2)
95600 SUB1 (RPLACD X2 (LIST X3))
95700 (SETQ X2 (CDR X2))
95800 SUB2 (SETQ Z (CDR Z))
95900 (SETQ Z4 (CAR Z))
96000 (COND ((NULL Z) (RETURN X1))
96100 ((EQ Z XX) (SETQ X3 TS) (GO SUB1))
96200 ((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
96300 ((CONST Z4) (SETQ X3 Z4) (GO SUB1))
96400 (T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
96500 EXPR)
96600
96700 (DEFPROP SUBS3T**
96800 (LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
96900 EXPR)
97000
97100 (DEFPROP SUB*
97200 (LAMBDA(X L)
97300 (PROG (S2 Z L1)
97400 B (SETQ L1 L)
97500 A (SETQ S2 (CDADAR L1))
97600 (SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
97700 (COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
97800 (SETQ L1 (CDR L1))
97900 (COND (L1 (GO A)))
98000 (SETQ X (CDR X))
98100 (COND (X (GO B)))))
98200 EXPR)
98300
98400 (DEFPROP SUBSKOL
98500 (LAMBDA (C EXL) (SUBS3T EXL C))
98600 EXPR)
98700
98800 (DEFPROP SUPPORT
98900 (LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
99000 EXPR)
99100
99200 (DEFPROP SUBSUME1
99300 (LAMBDA(C CB D DB L)
99400 (PROG (Z)
99500 SUB5 (COND ((NEG (CAR C)) (GO SUB3))
99600 ((NEG (CAR D)) (RETURN NIL))
99700 ((EQ (CAAR C) (CAAR D)) (GO SUB1))
99800 ((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
99900 (T (GO SUB2)))
00100 SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
00200 SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
00300 SUB2 (SETQ D (CDR D))
00400 (COND (D (SETQ DB (CDR DB)) (GO SUB5)))
00500 (RETURN NIL)
00600 SUB3 (COND
00700 ((NEG (CAR D))
00800 (COND ((EQ (CADAR C) (CADAR D))
00900 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
01000 (T (GO SUB2))))
01100 ((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
01200 (T (GO SUB2)))))
01300 (SETQ D (CDR D))
01400 (COND (D (SETQ DB (CDR DB)) (GO SUB3)))
01500 (RETURN NIL)))
01600 EXPR)
01700
01800 (DEFPROP SUBS2T
01900 (LAMBDA(X Y Z)
02000 (PROG (U Z1)
02100 (COND ((EQ X Y) (RETURN Z)))
02200 (SETQ U (CDR Z))
02300 (GO S2)
02400 S1 (SETQ Z1 (CDAR U))
02500 (COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
02600 ((CONST Z1) NIL)
02700 (T (RPLACD (CAR U) (S2 X Y Z1))))
02800 (SETQ U (CDR U))
02900 S2 (COND (U (GO S1)))
03000 (RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
03100 (RETURN Z)))
03200 EXPR)
03300
03400 (DEFPROP SUBS3T
03500 (LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
03600 EXPR)
03700
03800 (DEFPROP SUBSUME
03900 (LAMBDA(C D)
04000 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
04100 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
04200 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
04300 (T NIL)))
04400 EXPR)
04500
04600 (DEFPROP SUBSUME*
04700 (LAMBDA (C D) (PROG NIL (RETURN (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))))
04800 EXPR)
04900
05000 (DEFPROP SUBST1
05100 (LAMBDA(X Y Z)
05200 (COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
05300 ((EQUAL Y Z) X)
05400 (T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
05500 EXPR)
05600
05700 (DEFPROP TCOPY
05800 (LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
05900 EXPR)
06000
06100 (DEFPROP TEMPLATE
06200 (LAMBDA(L)
06300 (PROG (NAME VARLIS Z Z1 Z2)
06400 (SETQ NAME (CAR L))
06500 (SETQ L (CADR L))
06600 (COND ((NOT (EQ (CAR L) (QUOTE LAMBDA))) (PRINT (QUOTE ERROR))))
06700 (SETQ VARLIS (CADR L))
06800 (SETQ L (CDDR L))
06900 P1 (COND ((NULL L) (GO P3)))
07000 (SETQ Z (MKPRED L))
07100 P2 (COND
07200 (Z (COND ((ATOM (CAAR Z)) (SETQ Z1 (NCONC Z1 (LIST Z)))) (T (SETQ Z1 (NCONC Z1 Z))))
07300 (SETQ L (CDDR L))
07400 (GO P1)))
07500 (SETQ L (CDR L))
07600 (COND ((NULL L) (GO P3)))
07700 (SETQ Z (MKPRED L))
07800 (SETQ Z2 (NCONC Z2 (LIST Z1)))
07900 (SETQ Z1 NIL)
08000 (COND (Z (GO P2)))
08100 P3 (PUTPROP NAME (QUOTE (LAMBDA (L) (CONS (QUOTE APPLYTEMP) L))) (QUOTE MACRO))
08200 (SETQ TEMPLATELIST (CONS (CONS NAME (CONS VARLIS Z2)) TEMPLATELIST))))
08300 FEXPR)
08400
08500 (DEFPROP TERMS
08600 (LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
08700 EXPR)
08800
08900 (DEFPROP TERMS1
09000 (LAMBDA(L N)
09100 (COND ((OR (ZEROP N) (NULL L)) NIL)
09200 ((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
09300 (T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
09400 EXPR)
09500
09600 (DEFPROP TERMS2
09700 (LAMBDA(Z L N)
09800 (PROG (Z1 T1 T2)
09900 (SETQ T2 (SETQ T1 (LIST NIL)))
10000 A (COND ((NULL L) (RETURN T1))
10100 ((VAR (CAR L)) (GO B))
10200 ((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
10300 ((EQ N 1) (GO B)))
10400 (SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
10500 (COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
10600 (COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
10700 B (SETQ L (CDR L))
10800 (GO A)))
10900 EXPR)
11000
11100 (DEFPROP TIMEIT
11200 (LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
11300 EXPR)
11400
11500 (DEFPROP TREE
11600 (LAMBDA(L)
11700 (COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
11800 (T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
11900 EXPR)
12000
12100 (DEFPROP TREEDEP
12200 (LAMBDA(X)
12300 (PROG (Z)
12400 (SETQ Z (ANCESTOR X))
12500 (COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
12600 EXPR)
12700
12800 (DEFPROP TRY
12900 (LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
13000 FEXPR)
13100
13200 (DEFPROP TRY1
13300 (LAMBDA(L)
13400 (PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
13500 (SETQ PRNO 0)
13600 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
13700 (SETQ Z (CAR (LAST L)))
13800 (SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
13900 (EVAL (CONS (QUOTE INPUT) L))
14000 (INC T)
14100 P3 B (SETQ Z2 (INCLAUSES))
14200 (INC NIL)
14300 (COND ((NULL Z2) (RETURN NIL)))
14400 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
14500 (SETQ Z2 (ATTEMPT Z2 NIL NIL))
14600 A (COND ((NULL Z2) (RETURN (QUOTE *)))
14700 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
14800 ((EQ (CAR Z2) (QUOTE ABORT))
14900 (SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
15000 (GO A)))
15100 FEXPR)
15200
15300 (DEFPROP TRYPRF
15400 (LAMBDA(U)
15500 (PROG (Z1 Z2 R)
15600 TRY4 TRY3
15700 (SETQ XX (CHOICE XX EE EE1))
15800 (COND ((NULL XX) (GO TRY7)) ((EQ XX T) (GO TRY7)))
15900 (SETQ Z1 (CAAR XX))
16000 (SETQ Z2 (CADR XX))
16100 (COND ((OR (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
16200 TRY2 TRY1
16300 (COND ((NOT STRATEGY) (GO TRY1A)))
16400 (COND ((STRATEGY Z1 Z2) (GO TRY1A)) (T (GO TRY6F)))
16500 TRY1A
16600 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
16700 (SETQ R (RESOLVE Z1 Z2))
16800 TRY10
16900 (COND ((NULL R) (GO TRY6A)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
17000 (SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
17100 TRY6A
17200 TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
17300 (SETQ R (PARMOD Z1 Z2))
17400 (COND ((NULL R) (GO TRY6F)))
17500 (SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
17600 TRY6F
17700 TRY6G
17800 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
17900 (GO TRY3)
18000 TRY7 (PRINT (QUOTE COUNT))
18100 (PRINT COUNT)
18200 (PRINT (QUOTE LEVEL))
18300 (PRINT LVL)
18400 (SETQ LVL (ADD1 LVL))
18500 (PRINT (QUOTE ELAPSED-TIME))
18600 (PRINT (TIMEIT))
18700 (SETQ EE EE1)
18800 (SETQ XX (CONS U EE))
18900 (COND ((CDR EE) (SETQ EE1 (LAST EE)) (GO TRY4)))
19000 (PRINT (QUOTE NO-PROOF-FOUND))
19100 (COND (AUTO (ERR (QUOTE NOPROOF))))
19200 (UPDATE CLAUSES)
19300 (ERR (QUOTE NOPROOF))
19400 TRY6H))
19500 EXPR)
19600
19700 (DEFPROP TRAVERSE
19800 (LAMBDA(L)
19900 (PROG (Z Z1 Z2)
20000 (SETQ Z (ANCESTOR L))
20100 (SETQ Z1 (CAR Z))
20200 (SETQ Z (CDR Z))
20300 (COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
20400 (COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
20500 (RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
20600 EXPR)
20700
20800 (DEFPROP UNIT
20900 (LAMBDA (X) (EQ (NUM X) 1))
21000 EXPR)
21100
21200 (DEFPROP UNITS
21300 (LAMBDA(U)
21400 (PROG (Z Z1)
21500 (COND ((NULL U) (RETURN NIL)))
21600 (SETQ Z U)
21700 UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
21800 (SETQ Z (CDR Z))
21900 (COND (Z (GO UN1)))
22000 (RETURN Z1)))
22100 EXPR)
22200
22300 (DEFPROP UNITRES
22400 (LAMBDA(C UP UN)
22500 (PROG (C1 Z1 U Z RES)
22600 (SETQ C1 C)
22700 (COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
22800 (COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
22900 (SETQ C (CDR C))
23000 B (SETQ Z1 (CAR C))
23100 (COND ((NEG Z1) (GO N)))
23200 (SETQ U UN)
23300 A (COND ((NOT (EQ (CAR Z1) (CADAR (CAR U)))) (GO A1)))
23400 (SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
23500 (COND ((NULL Z) (GO A1)))
23600 (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
23700 (SETQ RES (CONS (REDUCER C1 C) RES))
23800 (GO A2)
23900 A1 (SETQ U (CDR U))
24000 (COND (U (GO A)))
24100 A2 (SETQ C (CDR C))
24200 (COND (C (GO B)) (T (RETURN RES)))
24300 N (SETQ Z1 (CDAR C))
24400 (SETQ U UP)
24500 C (COND ((NULL U) (RETURN RES)))
24600 C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
24700 (SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
24800 (COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
24900 (SETQ RES (CONS (REDUCER C1 C) RES))
25000 (GO C3)
25100 C1 (SETQ U (CDR U))
25200 (COND (U (GO C2)))
25300 C3 (SETQ C (CDR C))
25400 (COND (C (GO N)) (T (RETURN RES)))))
25500 EXPR)
25600
25700 (DEFPROP UNITREDUCT
25800 (LAMBDA(R UP UN)
25900 (PROG (Z UP1 UN1 C1 C2 RC1 RC2)
26000 (SETQ UN1 (SETQ UP1 NIL))
26100 (SETQ C1 (SETQ C2 R))
26200 A (SETQ RC1 (SETQ RC2 NIL))
26300 (COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
26400 B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
26500 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
26600 ((NULL (CAR Z)) (RETURN (LIST NIL)))
26700 (T (SETQ RC1 (APPEND Z RC1))))
26800 (SETQ C2 (CDR C2))
26900 (COND (C2 (GO B)))
27000 C1 (SETQ UP (APPEND UP1 UP))
27100 (SETQ UN (APPEND UN1 UN))
27200 C (SETQ Z (UNITRES (CAR C1) UP UN))
27300 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
27400 ((NULL (CAR Z)) (RETURN (LIST NIL)))
27500 (T (SETQ RC1 (APPEND Z RC1))))
27600 (SETQ C1 (CDR C1))
27700 (COND (C1 (GO C)))
27800 (COND ((NULL RC1) (RETURN RC2)))
27900 (SETQ C2 RC2)
28000 (SETQ C1 RC1)
28100 (SETQ Z (UNITPN C1))
28200 (COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
28300 (SETQ UP1 (CAR Z))
28400 (SETQ UN1 (CDR Z))
28500 (GO A)))
28600 EXPR)
28700
28800 (DEFPROP UNITPN
28900 (LAMBDA(X)
29000 (PROG (P N)
29100 A (COND
29200 ((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
29300 (SETQ X (CDR X))
29400 (COND (X (GO A)))
29500 (RETURN (CONS P N))))
29600 EXPR)
29700
29800 (DEFPROP UNIFY
29900 (LAMBDA(X Y)
30000 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
30100 (SETQ LC (LIST NIL))
30200 U3 (SETQ Z1 (CAR X))
30300 (SETQ Z2 (CAR Y))
30400 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
30500 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
30600 (COND ((VAR Z3)
30700 (COND ((VAR Z4) (GO UN1))
30800 ((CONST Z4) (GO UN3))
30900 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
31000 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
31100 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
31200 ((VAR Z4)
31300 (COND ((CONST Z3) (GO UN1))
31400 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
31500 ((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
31600 (COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
31700 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
31800 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
31900 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
32000 (SETQ X (APPEND Z6 (CDR X)))
32100 (SETQ Y (APPEND Z7 (CDR Y)))
32200 (GO U3))
32300 (T (RETURN NIL)))
32400 UN1 (SUBS2T Z3 Z4 LC)
32500 UN2 (SETQ X (CDR X))
32600 (COND (X (SETQ Y (CDR Y)) (GO U3)))
32700 (RETURN LC)
32800 UN3 (SUBS2T Z4 Z3 LC)
32900 (GO UN2)))
33000 EXPR)
33100
33200 (DEFPROP UNI
33300 (LAMBDA(C D L)
33400 (PROG (Z1 Z2 Z3)
33500 UN2 (SETQ Z2 (CAR D))
33600 (SETQ Z1 (SETQ Z3 (CAR C)))
33700 (COND
33800 ((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
33900 (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
34000 ((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
34100 (COND ((VAR Z2) (RETURN NIL))
34200 ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
34300 ((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
34400 ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
34500 (SETQ D (APPEND (CDR Z2) (CDR D)))
34600 (GO UN2))
34700 (T (RETURN NIL)))
34800 UN1 (SETQ C (CDR C))
34900 (COND (C (SETQ D (CDR D)) (GO UN2)))
35000 (COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
35100 EXPR)
35200
35300 (DEFPROP UNION
35400 (LAMBDA(Z C D YC YD)
35500 (PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
35600 (SETQ NO* NO)
35700 (COND
35800 (ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
35900 (COND ((< L (CDR SAT)) (RETURN NIL)))))
36000 (SETQ M1 0)
36100 (SETQ Z7 (ANCESTOR C))
36200 (SETQ Z8 (ANCESTOR D))
36300 (SETQ C (CDR C))
36400 (SETQ D (CDR D))
36500 (SETQ Z1 Z)
36600 (SETQ Z2 Z)
36700 (SETQ Z3 (SUBS3T** Z1 YC))
36800 (SETQ Z4 (SUBS3T** Z2 YD))
36900 UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
37000 (COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
37100 ((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
37200 (SETQ C1 (CONS Z5 C1))
37300 UN1A (SETQ C (CDR C))
37400 (COND (C (GO UN1)))
37500 UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
37600 (COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
37700 ((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
37800 ((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
37900 ((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
38000 UN2B (SETQ C2 (CONS Z6 C2))
38100 UN2A (SETQ D (CDR D))
38200 (COND (D (GO UN2)))
38300 (SETQ Z2 0)
38400 (COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
38500 ((NULL C2) (SETQ Z1 C1) (GO UN7)))
38600 (COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
38700 UN5 (SETQ NEG RES)
38800 (COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
38900 ((NULL C2) (SETQ Z1 C1) (GO UN7))
39000 ((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
39100 ((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
39200 ((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
39300 (SETQ Z1 (CAR C1))
39400 (SETQ C1 (CDR C1))
39500 (GO UN4)))
39600 UN6 (SETQ Z1 (CAR C2))
39700 (SETQ C2 (CDR C2))
39800 UN4 (UPIT Z1)
39900 (COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
40000 UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
40100 (SETQ Z2 (ADD1 Z2))
40200 (UPIT (CAR Z1))
40300 (SETQ RES (CONS (CAR Z1) RES))
40400 (COND ((NEG (CAR Z1)) (SETQ NEG RES)))
40500 UN8 (SETQ Z1 (CDR Z1))
40600 (GO UN7)
40700 UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
40800 (SETQ Z1 (CAR C2))
40900 (SETQ C2 (CDR C2))
41000 UN4A (UPIT1 (CDR Z1))
41100 (COND ((MEMBER Z1 RES) (GO UN5A)))
41200 (SETQ Z2 (ADD1 Z2))
41300 (SETQ RES (CONS Z1 RES))
41400 UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
41500 (GO UN3)))
41600 EXPR)
41700
41800 (DEFPROP UNWIND
41900 (LAMBDA(X1 X2 Y Z N)
42000 (PROG (Z1 Z2)
42100 (SETQ Z2 (ASSOC1 X1 Z))
42200 (COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
42300 (NCONC Y (COPYDELETED X1))
42400 (NCONC Z (LIST (CONS (LAST Y) N)))
42500 (SETQ Z1 N)
42600 (SETQ N (ADD1 N))
42700 A (SETQ Z2 (ASSOC1 X2 Z))
42800 (COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
42900 (NCONC Y (COPYDELETED X2))
43000 (NCONC Z (LIST (CONS (LAST Y) N)))
43100 (RETURN (CONS (CONS Z1 N) (ADD1 N)))))
43200 EXPR)
43300
43400 (DEFPROP UPDATE
43500 (LAMBDA(E)
43600 (PROG (USINGFL USING
43700 CHAN1
43800 ELOC
43900 CHAN
44000 AUTO
44100 DL1
44200 RF
44300 XYZ
44400 XYZ1
44500 CMD
44600 LOCFLG
44700 Z
44800 Z1
44900 Z2
45000 INCT
45100 Z3
45200 UEX
45300 Z1R
45400 Z2R
45500 N1
45600 R
45700 N
45800 NAME
45900 NAMELIST
46000 ZZ)
46100 (SETQ CHAN (OUTC NIL NIL))
46200 (SETQ AXNO (QUOTE INSERT))
46300 (SETQ FNNAM (QUOTE EDI))
46400 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
46500 (SETQ N1 (LAST NAMELIST))
46600 (SETQ INCT (INC NIL))
46700 U9 (SETQ ELOC E)
46800 (SETQ N 1)
46900 U3 (UP1A (CAR ELOC) N)
47000 U3A (TERPRI)
47100 U3AA (SETQ CMD (READ))
47200 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
47300 U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
47400 U3C (SETQ CMD (EXPLODE CMD))
47500 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
47600 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
47700 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
47800 (GO U3A)
47900 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
48000 (GO U3A)
48100 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
48200 (COND ((NULL Z1) (GO U3A)))
48300 (CLAUSES Z1)
48400 (GO U3A)
48500 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
48600 (SETQ Z NAMELIST)
48700 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
48800 (SETQ Z (CDR Z))
48900 (COND (Z (GO USY2)))
49000 (GO U3A)
49100 UFL2 (SETQ Z (QUOTE U))
49200 (GO UFL4)
49300 UFL3 (SETQ Z (QUOTE D))
49400 (GO UFL4)
49500 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
49600 UFL4 (SETQ Z2 405104)
49700 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
49800 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
49900 (COND ((OR (NULL Z) (EQ (CAR Z )(QUOTE ABORT))) (GO U3A)))
50000 (UPDATESTATE (CDDR Z))
50100 (GO U3A)
50200 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
50300 (COND ((NULL Z2) (GO U3A)))
50400 (EXPUNGE Z2)
50500 (GO U3A)
50600 UIN1 (SETQ NAME (READ))
50700 (SETQ Z2 (UPGETL E NAMELIST))
50800 (COND ((NULL Z2) (GO U3A)))
50900 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
51000 (NCONC Z1 Z2)
51100 (GO U3A)
51200 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
51300 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
51400 ((NULL (CAR Z1)) (GO U3A)))
51500 (SETQ Z3 NIL)
51600 (SETQ Z1 (CAR Z1))
51700 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
51800 (SETQ Z1 (CDR Z1))
51900 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (GO U12B)))
52000 UUP1 (SETQ Z2 (UPGETNU))
52100 (COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
52200 UDO1 (SETQ Z2 (UPGETNU))
52300 (COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
52400 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
52500 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
52600 (SETQ Z2 (CDR Z2))
52700 (GO UAN2)
52800 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
52900 (INC INCT)
53000 (OUTC CHAN NIL)
53100 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
53200 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
53300 (RETURN (MINIMIZE (APPEND Z1 Z)))
53400 USA1 (SETQ Z2 (UPGETL E NAMELIST))
53500 (COND (Z2 (NCONC E Z2)))
53600 (GO U3A)
53700 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
53800 (SETQ Z2 (UPGETL E NAMELIST))
53900 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
54000 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
54100 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
54200 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
54300 (SETQ Z3 Z1)
54400 USI2 (DEMOD (LIST (CAR Z3)) Z2)
54500 (SETQ Z3 (CDR Z3))
54600 (COND (Z3 (GO USI2)))
54700 (PRINT (QUOTE CLAUSES-ARE:))
54800 (CLAUSES Z1)
54900 (GO U3A)
55000 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
55100 (GO UUS3)
55200 UCU1 (QUERY)
55300 (GO U3A)
55400 UDS1 (SETQ Z1 (READ))
55500 (COND ((NOT (ATOM Z1)) (GO UDS3)))
55600 UDS2 (COND
55700 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
55800 (GO UDS2)))
55900 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
56000 (GO U3A)
56100 UEO1 (OUTC CHAN1 T)
56200 (GO U3A)
56300 UUS1 (SETQ NAME (QUOTE %USING))
56400 (SETQ USINGFL T)
56500 (SETQ USING NIL)
56600 UUS3 (SETQ LOCFLG T)
56700 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
56800 (SETQ USINGFL NIL)
56900 (COND ((NULL Z2) (GO U3A)))
57000 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
57100 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
57200 (T (RPLACA (CAR N1) NAME)
57300 (RPLACD (CAR N1) Z2)
57400 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
57500 (SETQ N1 (CDR N1))))
57600 (GO U3A)
57700 USE1 (SETQ NAME (READ))
57800 (SETQ LOCFLG NIL)
57900 (GO UUS2)
58000 UCL1 (SETQ Z (READ))
58100 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
58200 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
58300 (GO UCL2))
58400 (T (GO U3A)))
58500 UGO1 (SETQ Z1 (UPGETNU))
58600 (COND ((NOT (NUMBERP Z1)) (GO U3A)))
58700 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
58800 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
58900 UTR1 (SETQ UEX NIL)
59000 (GO UEX2)
59100 UEX1 (SETQ UEX T)
59200 UEX2 (SETQ NAME (QUOTE LEMMA))
59300 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
59400 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
59500 (SETQ AUTO T)
59600 (SETQ Z2
59700 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
59800 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
59900 (T NIL))
60000 NIL))
60100 (SETQ AUTO NIL)
60200 (GO AT1A)
60300 UST1 (STOP)
60400 (GO U3A)
60500 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
60600 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
60700 U8 (COND ((EQ Z2 0) (GO U9)))
60800 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
60900 (SETQ Z2 (DIFFERENCE Z2 5))
61000 (SETQ ZZ 5)
61100 U84 (SETQ Z N)
61200 (SETQ Z3 (DIFFERENCE N ZZ))
61300 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
61400 (SETQ N Z3)
61500 (SETQ Z3 ELOC)
61600 (SETQ ELOC (DOWN N E))
61700 (SETQ ZZ NIL)
61800 (SETQ Z1 ELOC)
61900 U81 (COND ((EQ Z1 Z3) (GO U82)))
62000 (SETQ ZZ (CONS (CAR Z1) ZZ))
62100 (SETQ Z1 (CDR Z1))
62200 (GO U81)
62300 U82 (COND ((NULL ZZ) (GO U83)))
62400 (UP1A (CAR ZZ) (SUB1 Z))
62500 (SETQ ZZ (CDR ZZ))
62600 (SETQ Z (SUB1 Z))
62700 (GO U82)
62800 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
62900 (SETQ Z2 (PLUS Z2 N))
63000 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
63100 (SETQ ELOC (CDR ELOC))
63200 (SETQ N (ADD1 N))
63300 (UP1A (CAR ELOC) N)
63400 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
63500 UPR1 (TERPRI)
63600 (SETQ Z2 (UPGETL E NAMELIST))
63700 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
63800 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
63900 (SETQ AXNO (QUOTE THEOREM))
64000 (SETQ Z3 (NEGATE (CAR Z2)))
64100 (SETQ AXNO (QUOTE INSERT))
64200 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
64300 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
64400 (SETQ NAME (QUOTE LEMMA))
64500 (SETQ LOCFLG T)
64600 (GO USE2)
64700 UME1 (SETQ Z1 (UPGETL E NAMELIST))
64800 (SETQ Z2 (UPGETL E NAMELIST))
64900 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
65000 (BAKSUB Z1 Z2)
65100 (GO U3A)
65200 UHE1 (PRINT MESSAGE)
65300 (GO U3A)
65400 URE1 (SETQ Z1 (UPGETL E NAMELIST))
65500 (SETQ Z2 (UPGETL E NAMELIST))
65600 U%RE1
65700 (SETQ RF T)
65800 URE1A
65900 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
66000 (SETQ Z1R Z1)
66100 (SETQ Z2R Z2)
66200 (SETQ Z3 NIL)
66300 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
66400 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
66500 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
66600 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
66700 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
66800 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
66900 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
67000 UR3A (SETQ Z2R (CDR Z2R))
67100 (COND (Z2R (GO UR3)))
67200 (SETQ Z1R (CDR Z1R))
67300 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
67400 UR3B (COND ((NULL Z3)
67500 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
67600 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
67700 (RF (SETQ NAME (QUOTE RES)))
67800 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
67900 (SETQ Z2 Z3)
68000 (SETQ LOCFLG T)
68100 (GO AT2A)
68200 UEV1 (PRINT (QUOTE EVAL-AWAITS))
68300 (SETQ Z2 (ERRSET (EVAL (READ)) T))
68400 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
68500 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
68600 (GO UEV1)
68700 UPDATE1
68800 (SETQ Z (EXPLODE (CAR CMD)))
68900 (COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
69000 AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
69100 (SETQ NAME (CADR CMD))
69200 (SETQ XYZ Z1)
69300 (RPLACA (CDR CMD) (QUOTE XYZ))
69400 (RPLACA CMD (QUOTE ATTEMPTUNTIL))
69500 (SETQ Z2 (EVAL CMD))
69600 AT1A (UPDATESTATE STRAT)
69700 (COND
69800 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
69900 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
70000 (PRINC NAME)
70100 (GO U3A))
70200 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
70300 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
70400 (SETQ AUTO NIL)
70500 (GO AT1A))
70600 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
70700 (SETQ Z2 (CADR Z2))
70800 AT2A (SETQ N 1)
70900 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
71000 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
71100 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
71200 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
71300 (PRIN1 NAME)
71400 (CLAUSES Z2)
71500 (GO USE2)
71600 S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
71700 (RPLACA (CDDDR CMD) (QUOTE XYZ))
71800 (RPLACA CMD (QUOTE SAVE))
71900 (EVAL CMD)
72000 (GO U3A)))
72100 EXPR)
72200
72300 (DEFPROP UPGETL
72400 (LAMBDA(E N)
72500 (PROG (C N1 Z Z1 Z2 Z3 ZZ N2)
72600 (SCANSET)
72700 (START)
72800 (SETQ C (ERRSET (<CLAUSES>) T))
72900 (SCANRESET)
73000 (COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
73100 (SETQ C (TOP))
73200 (COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
73300 AS1 (SETQ Z (CAR C))
73400 (COND ((ATOM Z)
73500 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
73600 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
73700 (T (RETURN NIL))))
73800 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
73900 (T (RETURN NIL))))
74000 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
74100 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
74200 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
74300 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
74400 (T (RETURN NIL)))
74500 AS6 (SETQ C (CDR C))
74600 (COND (C (GO AS1)) (T (RETURN ZZ)))
74700 AS2 (SETQ Z2 (CADR Z))
74800 (SETQ N1 (CAR Z))
74900 (SETQ Z (CDR Z))
75000 (SETQ Z3 Z1)
75100 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
75200 AS3 (SETQ Z2 (SUB1 Z2))
75300 (COND ((ZEROP Z2) (GO AS4)))
75400 (SETQ Z1 (CDR Z1))
75500 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
75600 AS4 (COND
75700 ((NOT (HERE (CAR Z1))) (PRINT N1)
75800 (PRINC (QUOTE / ))
75900 (PRINC (CAR Z))
76000 (PRINC (QUOTE / ))
76100 (PRINC (QUOTE HAS-BEEN-DELETED))
76200 (RETURN NIL)))
76300 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
76400 (SETQ Z (CDR Z))
76500 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
76600 (GO AS6)
76700 AS10 (SETQ N2 (QUOTE INSERT))
76800 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (FIXQFF (CDR Z)))))))
76900 (GO AS6)
77000 AS20 (SETQ N2 (QUOTE MATCHES))
77100 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
77200 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
77300 AS30 (SETQ N2 (QUOTE INPUT))
77400 (SETQ ZIN (CDR Z))
77500 (COND
77600 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
77700 (INC T)
77800 (SETQ Z (INCLAUSES))
77900 (INC NIL)
78000 (COND ((NULL Z) (RETURN NIL)))
78100 AS31 (SETQ ZZ (APPENDIT ZZ Z))
78200 (GO AS6)))
78300 EXPR)
78400
78500 (DEFPROP UPGETNU
78600 (LAMBDA NIL
78700 (PROG (Z)
78800 (SETQ Z (READ))
78900 A (COND ((NUMBERP Z) (RETURN Z)))
79000 (SETQ Z (REVERSE (EXPLODE Z)))
79100 (COND ((EQ (CAR Z) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z)))) (GO A)) (T (RETURN NIL)))))
79200 EXPR)
79300
79400 (DEFPROP UPDATESTATE
79500 (LAMBDA(L)
79600 (PROG (L1)
79700 (SETQ L1 STATEVECTOR)
79800 A (COND ((NULL L) (RETURN NIL)))
79900 (SET (CAR L1) (CAR L))
80000 (SETQ L (CDR L))
80100 (SETQ L1 (CDR L1))
80200 (GO A)))
80300 EXPR)
80400
80500 (DEFPROP UPIT
80600 (LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
80700 EXPR)
80800
80900 (DEFPROP UPIT1
81000 (LAMBDA(Z)
81100 (PROG (Z1 Z2)
81200 MAX2 (SETQ Z2 (CAR Z))
81300 (COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
81400 ((GREATERP Z2 NO*) NIL)
81500 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
81600 (GO MAX1))
81700 ((CONST Z2) (GO MAX1))
81800 (T (UPIT1 (CDR Z2))))
81900 MAX1 (SETQ Z (CDR Z))
82000 (COND (Z (GO MAX2)))
82100 (RETURN NO)))
82200 EXPR)
82300
82400 (DEFPROP UP1A
82500 (LAMBDA(X N)
82600 (PROG NIL
82700 (TERPRI)
82800 (PRINC N)
82900 (PRINC (QUOTE / ))
83000 (COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
83100 (RETURN NIL)))
83200 EXPR)
83300
83400 (DEFPROP UP1B
83500 (LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
83600 EXPR)
83700
83800 (DEFPROP VARIT
83900 (LAMBDA(Z)
84000 (PROG (Z1 Z2 BL Z3)
84100 (SETQ Z3 Z)
84200 M1 (SETQ Z2 (CAR Z))
84300 (COND ((VAR Z2)
84400 (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
84500 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
84600 ((EQ (CAR Z2) (QUOTE _)) (RPLACA Z (SETQ NO (ADD1 NO))))
84700 ((CONST Z2) NIL)
84800 (T (VARIT (CDR Z2))))
84900 (SETQ Z (CDR Z))
85000 (COND (Z (GO M1)))
85100 (RETURN Z3)))
85200 EXPR)
85300
85400 (DEFPROP VINE
85500 (LAMBDA (X) (NUMBERP (CDR (ANCESTOR X))))
85600 EXPR)
85700
85800 (DEFPROP <
85900 (LAMBDA(L X)
86000 (PROG (Z Z1 Z2)
86100 (SETQ Z X)
86200 (COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
86300 A1 (SETQ Z1 (CAR Z))
86400 (COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
86500 (COND ((NOT (ORDERP L Z1)) (GO A2))
86600 ((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
86700 A2 (SETQ Z (CDR Z))
86800 (COND (Z (GO A1)))
86900 (RETURN NIL)))
87000 EXPR)